So far we have introduced and studied normal forms for relational data and XML documents. Both are technologies to store and exchange information. XML documents are mainly used in the World Wide Web. As the World Wide Web evolves to the Semantic Web \cite{2001semanticweb, 2006semanticweb}, information evolves as well. Information stored with the relational model is represented as tables, information stored in XML documents as trees, and the information stored in the Semantic Web as a graph. Therefore, the data models used in the Semantic Web can be seen as graph databases. \\

\noindent The W3C consortium started an initiative to standardize data models in the Semantic Web. As a result the Resource Description Framework (RDF) \cite{2004rdf} was created as a formal language for describing structured information \cite{2010foundsemweb}. An RDF document can be viewed as a directed, labeled graph. Each resource is identified by a node. Nodes can be linked by directed edges. These edges are labeled, and describe the relationship between two nodes. The edge label is in RDF called \emph{predicate}. Such a binary relationship between two resources is denoted in RDF by a \emph{triple}. A triple consists of a \emph{subject} $s$ connected by a \emph{predicate} $p$ to an \emph{object} $o$, which is denoted by $\left(s,p,o\right)$. For example, the resource $p1$ in Figure~\ref{fig:gdb_articles} is connected via the $\rfo{has\_article}$ relation to the resource $a1$, which is denoted by the RDF triple:
$$\left(p1,has\_article,a1\right)$$
Additionally, semantic information can be attached to the nodes by means of an ontology. The most simple form of semantic information is to ``type'' resources. That is, we associate to a resource a specific class. This form of reasoning is already available in the RDF standard via the relation \texttt{rdf:type}, e.g. $\left(p1,\texttt{rdf:type},\cfo{proc}\right)$. In all figures we use UML like annotations of class membership, i.e.\ instead of a binary relation to a node denoting the class, we write $resource: \cfo{type}$. For example, in Figure~\ref{fig:gdb_articles} we write $p1 : \cfo{proc}$ to denote that the resource $p1$ is of type $\cfo{proc}$. \\

\noindent A simple ontology language is RDF Schema (RDF(S)) \cite{2004rdfs}. With RDF(S) we can attach even more semantic information to resources and roles. For example, we can specify that a resource is a class, e.g. $\left(\cfo{proc},\texttt{rdf:type},\texttt{rdfs:class}\right)$. Furthermore, we can type predicates, i.e.\ we can specify domain and range of predicates. For example, the predicate $\rfo{has\_article}$ has the domain $\cfo{proc}$ and the range $\cfo{article}$:
\begin{gather*}
 \left(\rfo{has\_article},\texttt{rdfs:domain},\cfo{proc}\right) \\
 \left(\rfo{has\_article},\texttt{rdfs:range},\cfo{article}\right)
\end{gather*}
Such information enables us to infer new information. For example, the above together with the triple $\left(p1,\rfo{has\_article},a1\right)$ infers: 
\begin{gather*}
 \left(p1,\texttt{rdf:type},\cfo{proc}\right) \\
 \left(a1,\texttt{rdf:type},\cfo{article}\right)
\end{gather*}

\noindent Even more semantic information can be attached to the data with the Web Ontology Language OWL \cite{2012owl} and OWL2 \cite{2012owl2semantics}. For example, OWL allows to state class disjointness. The semantics of these languages is best captured by Description Logics (DLs). Description Logics are a decidable fragment of first-order predicate logic and well-suited as a dependency language for graph databases. In this chapter we will discuss and introduce a normal form for DLs. We want to view redundancies and normal forms from a relational perspective. Therefore, we choose the DL $\DLA$. $\DLA$ is the formal model for the OWL2 profile OWL2 QL \cite{2012owl2prof}, which is particular well-suited to query data stored in relational databases. Additionally, $\DLA$ has just enough expressivity for conceptual modeling \cite{2005berardi, 2009calvanese}. \\

\noindent We will introduce in Section~\ref{sec:dl_pre} the Description Logic $\DLA$ as a formal model for graph-databases. Section~\ref{sec:dl_map} will then extend the ``Direct Mapping of Relational Data to RDF'' to map relational data into $\DLA$ KBs. Data dependencies for $\DLA$ are discussed in Section~\ref{sec:dl_fd}. Finally, a normal form for $\DLA$ extended with data dependencies is proposed in Section~\ref{sec:dl_nf} and Section~\ref{sec:dl_bcnf} shows that this normal form is a generalization of BCNF.

\begin{section}{Preliminaries}
\label{sec:dl_pre}

\begin{subsection}{The Description Logic $\DLA$}
\noindent Description Logics (DLs) \cite{2003baader} were developed as a formal language for structured knowledge representation (KR). The goal of KR is to ``develop formalisms for providing high-level descriptions of the world that can be effectively used to build intelligent applications'' \cite{2003baader, 2009baader}. DLs try to fulfill this goal. First, DLs provide us with a method to model important notions of a domain in terms of concept \textit{descriptions}. The basic components of DLs are \textit{concepts}, representing sets of objects and \textit{roles}, which establish relationships between (instances of) concepts. The knowledge in DLs is separated into terminological knowledge, stored in an TBox and assertional knowledge, represented by an ABox. The TBox specifies general properties of concepts and roles. The ABox describes individual objects and their relationship. Second, the \textit{logic}-based semantics of DLs allows us to infer new knowledge. These reasoning services include concept and role subsumption, knowledge base satisfiability and instance checking. The study of DLs in terms of expressivity and computational complexity of reasoning is one of the most important issues in DL research. \\

\noindent We will introduce $\DLA$ \cite{2006calvanese, 2008poggi}, a DL of the $\DL$ family \cite{2007calvanese2, 2009artale,  2013calvanese}. The advantage of the $\DL$ family is its low complexity of reasoning. For example, instance checking and query answering can be done in \LOGSPACE with respect to data complexity. Still it is possible to capture conceptual data models and object-oriented formalisms \cite{2006calvanese}. 

\begin{subsubsection}{Syntax of $\DLA$}
In comparison to the other DLs in the $\DL$ family, $\DLA$ distinguishes between \textit{objects} and \textit{values}. Therefore, our domain of interest is represented in terms of \textit{concepts} and \textit{roles}. Additionally, we introduce \textit{value-domains} which denote a set of (data) values and \textit{attributes}, which denote a binary relation between objects and values. The building blocks of $\DLA$ are \textit{atomic} concepts $A$,$A_1$,$\ldots$,$A_n$, atomic roles $P$,$P_1$,$\ldots$,$P_n$ and atomic attributes $U$,$U_1$,$\ldots$,$U_n$. All of them are denoted by a name. All names of attributes, and no other names, start with an $@$. From these we build complex concepts, roles, value-domains and attributes according to the following syntax:

\begin{center}
\begin{tabular}{r|c|l|l}
 & atomic & basic & arbitrary \\
 \hline concept & $A$ & $B \ra A \mid \exists Q \mid \delta(U)$ & $C \ra B \mid \neg B$ \\
 role & $P$ & $Q \ra P \mid P^-$ & $R \ra Q \mid \neg Q$ \\
 value-domain & & $E \ra \rho(U)$ & $F \ra \top_D \mid T_1 \mid \ldots \mid T_n$ \\
 attribute & U & $V \ra U$ & $W \ra V \mid \neg V$ 
\end{tabular} 
\end{center}

\noindent We denote by $B$,$B_1$,$\ldots$,$B_n$ \textit{basic} concepts. A basic concept is either an atomic concept, the \textit{domain} of a role $Q$ ($\exists Q$), also called unqualified existential restriction, or the domain of an attribute $U$ ($\delta(U)$). An \textit{arbitrary} concept, denoted by $C$,$C_1$,$\ldots$,$C_n$, is built from a basic concept or its \textit{negation}. \\

\noindent A \textit{basic} role, denoted by $Q$,$Q_1$,$\ldots$,$Q_n$, is either an atomic role or the \textit{inverse} of an atomic role ($P^-$). An \textit{arbitrary} role can in addition to a basic role also be the negation of a basic role. In the following, when Q is a basic role, the expression $Q^-$ stands for $P^-$ when $Q = P$, and for $P$ when $Q = P^-$. \\

\noindent A \textit{basic} value-domain $E$ is given by the \textit{range} of an atomic attribute $U$. \textit{Arbitrary} value-domains are either the universal value-domain $\top_D$, or one of $n$ pairwise disjoint unbounded value-domains $T_1, \ldots, T_n$, which correspond to RDF data types, such as \texttt{xsd:string}, etc.

\begin{example}
\label{ex:dl_terms}
Let us model the same information given in Figure~\ref{fig:relCourse}. We need the following atomic concepts: $\cfo{course}$ represents a course, $\cfo{type}$ a course type, $\cfo{room}$ a room, and $\cfo{building}$ a building. We connect these atomic concepts using the atomic roles: $\rfo{located}$, $\rfo{has\_room}$ and $\rfo{for}$. With the atomic attribute $\rfo{@name}$ we attach a name value to different concepts. 
\end{example}

\noindent With those expressions it is possible, like in any other DL, to represent the domain of discourse in terms of a knowledge base $\mcK$. The KB $\mcK$ has two components. The TBox $\mcT$ consists of a finite set of intensional assertions. Intensional assertions describe the world in more general terms, for example ``Birds can fly.''. The ABox $\mcA$ consists of a finite set of extensional assertions, which describe individuals, for example ``Tweety is a bird''. Therefore, we often write $\mcK = \left< \mcT, \mcA \right>$. The TBox $\mcT$ consists of assertions of the form:

\begin{center}
\begin{tabular}{rcl@{\hskip 0.5in}l}
   $B$ & $\sqsubseteq$ & $C$ & concept inclusion\\
   $Q$ & $\sqsubseteq$ & $R$ & role inclusion\\
   $E$ & $\sqsubseteq$ & $F$ & value-domain inclusion\\
   $U$ & $\sqsubseteq$ & $V$ & attribute inclusion\\
   \multicolumn{3}{c@{\hskip 0.5in}}{$\funct{Q}$} & role functionality\\
   \multicolumn{3}{c@{\hskip 0.5in}}{$\funct{U}$} & attribute functionality
\end{tabular}
\end{center}

\noindent Intuitively, the above inclusion assertions state that each instance of the concept, role, value-domain or attribute on the left-hand side is also an instance of the right-hand side. We call inclusion assertions without negation (``$\neg$'') on the right-hand side \textit{positive inclusions} (PIs), and the others \textit{negative inclusions} (NIs). For example, the RDF triple \texttt{<has\_article> rdfs:domain <proc>} would be represented by the assertion $\cfo{proc} \sqsubseteq \exists \rfo{has\_article}$. \\

\noindent Functionality assertions ($\funct{Q}$ or $\funct{U}$) express that in every model of $\mcT$ the first component of a role (or attribute) determines the second component, i.e.\ this binary relation is a function. \\

\noindent The following conditions must be satisfied by every $\DLA$ TBox $\mcT$. These are crucial for the tractability of reasoning in $\DLA$ \cite{2008poggi}:

\begin{itemize}
    \item for each atomic role $P$, if either $\left( \mbox{funct } P \right)$ or $\left( \mbox{funct } P^- \right)$ occurs in $\mcT$, then $\mcT$ does not contain assertions of the form $Q^\prime \sqsubseteq P$ or $Q^\prime \sqsubseteq P^-$, where $Q^\prime$ is a basic role. 
    \item for each atomic attribute $U$, if $\left( \mbox{funct } U \right)$ occurs in $\mcT$, then $\mcT$ does not contain assertions of the form $U^\prime \sqsubseteq U$, where $U^\prime$ is an atomic attribute.
 \end{itemize}
 
\begin{example}
\label{ex:dl_tbox}
Let us model a TBox $\mcT_c$ for the information given in Figure~\ref{fig:relCourse}. We will use the concepts and roles given in Example~\ref{ex:dl_terms}. 

\begin{align*}
 \cfo{room} & \sqsubseteq \exists \rfo{for} & \exists \rfo{for} & \sqsubseteq \cfo{room} & \exists \rfo{for}  & \sqsubseteq \cfo{type}  \\
 \cfo{course} & \sqsubseteq \exists \rfo{located} &  \exists \rfo{located} & \sqsubseteq \cfo{course} & \exists \rfo{located}^-  & \sqsubseteq \cfo{room} \\
 \cfo{room} & \sqsubseteq \exists \rfo{has\_room}^- & \exists \rfo{has\_room} & \sqsubseteq \cfo{building} & \exists \rfo{has\_room}^-  & \sqsubseteq \cfo{room}  \\
 \cfo{course} & \sqsubseteq \neg \cfo{room} & \cfo{course} & \sqsubseteq \neg \cfo{type} & \cfo{course} & \sqsubseteq \neg \cfo{building}\\
 \cfo{room} & \sqsubseteq \neg \cfo{building} & \cfo{room} & \sqsubseteq \neg \cfo{type} & \cfo{building} & \sqsubseteq \neg \cfo{type} \\
 \cfo{course} & \sqsubseteq \delta(\rfo{@name}) & \cfo{type} & \sqsubseteq \delta(\rfo{@name}) & \rho\left(\rfo{@name}\right) & \sqsubseteq \mathtt{xsd:string} \\
 \cfo{room} & \sqsubseteq \delta(\rfo{@name}) & \cfo{building} & \sqsubseteq \delta(\rfo{@name}) 
\end{align*}
\begin{align*}
 & \funct{\rfo{for}} &  \funct{\rfo{located}} \\
 & \funct{\rfo{has\_room}^-} & \funct{\rfo{@name}} & \qedhere
\end{align*}
\end{example}

\noindent So far we have defined expressions and assertions that represent the domain of discourse in general. The $\DLA$ ABox allows us to express properties about different individuals. First, we need to define constants that represent such individuals. Let this set of constants be denoted by $\Gamma$. $\Gamma$ is partitioned into two sets, $\Gamma_V$ (for the set of constant symbols for values) and $\Gamma_O$ (for the set of constant symbols for objects). A $\DLA$ ABox consists of a finite set of \textit{membership assertions} of the form 

\begin{center}
\begin{tabular}{c@{\hskip 0.5in}c@{\hskip 0.5in}c@{\hskip 0.5in}}
  $A(a)$, & $P(a,b)$, & $U(a,v)$,
\end{tabular}
\end{center}

\noindent where $A$, $P$, and $U$ are an atomic concept, atomic role and atomic attribute, respectively. The constant symbols $a$ and $b$ are from $\Gamma_O$ and $v$ is from $\Gamma_V$. \\

\noindent We will denote by $\ffo{sign}^C\left(\mcK\right)$  the set of all atomic concepts in a KB $\mcK$ and by $\ffo{sign}^R\left(\mcK\right)$ the set of all atomic roles. We call $\ffo{sign}\left(\mcK\right) = \ffo{sign}^C\left(\mcK\right) \cup \ffo{sign}^R\left(\mcK\right)$ the signature of a KB $\mcK$.

\begin{example}
\label{ex:dl_abox}
We continue Example~\ref{ex:dl_tbox} and specify membership assertions to represent the information given in Figure~\ref{fig:relCourse}. We have the following sets of constant symbols:
\begin{items} 
 \item $\{ c1, c2, c3, t1, t2, r1, r2, b1, b2 \} \subseteq \Gamma_O$
 \item $\{ \textnormal{``Algebra I''}, \textnormal{``Economics I''}, \textnormal{``VO''}, \textnormal{``UE''},\textnormal{``SEM1''}, \textnormal{``HS1''}, \textnormal{``Main''}, \textnormal{``Dep''} \} \subseteq \Gamma_V$
\end{items}

\noindent The $\DLA$ ABox $\mcA_c$ consists of the following assertions:

\begin{center}
\begin{tabular}{lll}
  $\cfo{course}\left(c1\right)$ & $\cfo{type}\left(t1\right)$ & $\cfo{room}\left(r1\right)$  \\
  $\cfo{course}\left(c2\right)$ & $\cfo{type}\left(t2\right)$ & $\cfo{room}\left(r2\right)$   \\
  $\cfo{course}\left(c3\right)$ & $\cfo{building}\left(b1\right)$ & $\cfo{building}\left(b2\right)$\\
  $\rfo{@name}\left(c1,\textnormal{``Algebra I''}\right)$ &  $\rfo{@name}\left(t1,\textnormal{``VO''}\right)$ & $\rfo{@name}\left(r1,\textnormal{``HS1''}\right)$  \\
  $\rfo{@name}\left(c2,\textnormal{``Algebra I''}\right)$ & $\rfo{@name}\left(t2,\textnormal{``UE''}\right)$ & $\rfo{@name}\left(r2,\textnormal{``SEM1''}\right)$  \\
  $\rfo{@name}\left(c3,\textnormal{``Economics I''}\right)$ & $\rfo{@name}\left(b1,\textnormal{``Main''}\right)$ & $\rfo{@name}\left(b2,\textnormal{``Dep''}\right)$\\
  $\rfo{located}\left(c1, r1\right)$ & $\rfo{located}\left(c2, r2\right)$ & $\rfo{located}\left(c3, r2\right)$ \\
  $\rfo{for}\left(r1, t1\right)$ & $\rfo{for}\left(r2, t2\right)$ \\
  $\rfo{has\_room}\left(b1, r1\right)$ & $\rfo{has\_room}\left(b2, r2\right)$
\end{tabular}
\end{center}

\noindent The $\DLA$ ABox $\mcA_c$ can also be represented as a graph. Such a graph is depicted in Figure~\ref{fig:ABox_course}. The KB $\mcK_c = \left< \mcT_c, \mcA_c \right>$ is a representation of the same information as given in Figure~\ref{fig:relCourse}.
\end{example}


\begin{figure}[t]
\begin{center}
\input{figures/dl/ex_abox.tikz} 
\end{center}
\caption{A graph representation of the ABox $\mcA_c$.} 
\label{fig:ABox_course}
\end{figure}


\end{subsubsection}

\begin{subsubsection}{Semantics of $\DLA$}
Now that we have fully defined the syntax of $\DLA$ we need to add meaning to the expressions and assertions. We define the semantics of $\DLA$ in terms of interpretations, which are first order structures.  A $\DLA$ \textit{interpretation} $\mcI = (\Delta^\mcI, \cdot^\mcI)$ consists of an \textit{interpretation domain} $\Delta^\mcI$ and an \textit{interpretation function} $\cdot^\mcI$. The interpretation domain $\Delta^\mcI$ is the disjoint union of two non-empty sets: the \textit{domain of objects} $\Delta^\mcI_O$ and the \textit{domain of values} $\Delta^\mcI_V$. The interpretation function $\cdot^\mcI$ assigns an element of $\Delta^\mcI$ to each constant in $\Gamma$, such that for all $a \in \Gamma_O$, $a^\mcI \in \Delta_O^\mcI$ and for all $c \in \Gamma_V$, $c^\mcI \in \Delta_V^\mcI$.  The DL $\DLA$ adopts the \textit{unique name assumption} (UNA), therefore we also assume that for each pair $a_1, a_2 \in \Gamma$, whenever $a_1 \neq a_2$, we have that $a_1^\mcI \neq a_2^\mcI$. Additionally, the interpretation function $\cdot^\mcI$ maps 

\begin{items}
  \item atomic concepts to subsets of the interpretation domain of objects, i.e.\ $$A^\mcI \subseteq \Delta_O^\mcI,$$
  \item atomic roles to subsets of the crossproduct of the interpretation domain of objects, i.e.\ $$P^\mcI \subseteq \Delta_O^\mcI \times \Delta_O^\mcI,$$
  \item atomic attributes to subsets of the crossproduct of the interpretation domain of objects and values, i.e.\ $$U^\mcI \subseteq \Delta_O^\mcI \times \Delta_V^\mcI,$$
  \item value-domains to subsets of the interpretation domain of values, i.e.\ 
  \begin{align*}
  T_i^\mcI &\subseteq \Delta_V^\mcI & \top_D^\mcI &= \Delta_V^\mcI.
  \end{align*}
\end{items}

\noindent All interpretations of a particular KB agree on the semantics of each value-domain $T_i$ and each constant in $\Gamma_V$. That is, each value domain $T_i$ is interpreted as the set of values $\ffo{val}\left(T_i\right)$ corresponding to the RDF data type, and each constant $c_i \in \Gamma_V$ is interpreted as one specific value, denoted by $\ffo{val}\left(c_i\right)$, in $\ffo{val}\left(T_i\right)$. \\

\noindent For complex concepts, complex roles and complex attributes the interpretation has to satisfy the following conditions (given that $o,o^\prime \in \Delta_O^\mcI$ and $v \in \Delta_V^\mcI$):
\begin{align*}
   \left(\exists Q\right)^\mcI &= \{o \mid \exists o^\prime.\left(o,o^\prime\right) \in Q^\mcI \} & \left(P^-\right)^\mcI &= \{\left(o,o^\prime\right) \mid \left(o^\prime,o\right) \in P^\mcI \} \\   
   \left(\delta\left(U\right)\right)^\mcI &= \{o\mid\exists v.\left(o,v\right)\in U^\mcI \} & \left(\neg Q\right)^\mcI &= \left(\Delta_O^\mcI \times \Delta_O^\mcI\right) \setmin Q^\mcI \\
   \left(\neg B\right)^\mcI &= \Delta_O^\mcI \setmin B^\mcI &  \left(\neg V\right)^\mcI &= \left(\Delta_O^\mcI \times \Delta_V^\mcI\right) \setmin V^\mcI \\
   \left(\rho\left(U\right)\right)^\mcI &= \{v\mid\exists o.\left(o,v\right) \in U^\mcI \} & 
\end{align*}

\noindent We now turn our attention to the assertions in a KB TBox and ABox. Let $\alpha$ be a TBox assertion. Then, we say an interpretation $\mcI$ \textit{satisfies} the TBox assertion $\alpha$, denoted by $\mcI \models \alpha$, as follows: 

\begin{items}
    \item let $\alpha = \alpha_1 \sqsubseteq \alpha_2$, then $\mcI \models \alpha_1 \sqsubseteq \alpha_2$, if $\alpha_1^\mcI \subseteq \alpha_2^\mcI$,
    \item let $\alpha = \funct\beta$, where $\beta$ is either $P, P^-, U$. Then, $\mcI \models \funct\beta$, if $(o,e_1) \in \beta^\mcI$ and $(o,e_2) \in \beta^\mcI$ implies $e_1 = e_2$, for each $o \in \Delta_O^\mcI$, and $e_1, e_2$ in either $\Delta_O^\mcI$ or $\Delta_V^\mcI$.
\end{items}

\noindent Let $\alpha$ be an ABox assertion. Then, we say an interpretation $\mcI$ \textit{satisfies} the ABox assertion $\alpha$, denoted by $\mcI \models \alpha$, as follows: 
    
\begin{items}
   \item let $\alpha = A(a)$, then $\mcI \models A(a)$, if $a^\mcI \in A^\mcI$, 
   \item let $\alpha = P(a,a^\prime)$, then $\mcI \models P(a,a^\prime)$, if $(a^\mcI,a^{\prime\mcI}) \in P^\mcI$,
   \item let $\alpha = U(a,c)$, then $\mcI \models U(a,c)$, if $(a^\mcI,c^\mcI) \in U^\mcI$.
\end{items}

\noindent We say an interpretation $\mcI$ is a \textit{model} of a $\DLA$ KB $\mcK = \left<\mcT, \mcA\right>$, denoted by $\mcI \models \mcK$, if $\mcI$ satisfies all the assertions in $\mcT$ and $\mcA$. 

\begin{example}
\label{ex:dl_int}
We will give an interpretation $\mcI_c$ for the KB given in Example~\ref{ex:dl_abox}. The interpretation $\mcI$ is constituted from a domain $\Delta^{\mcI_c}$ and an interpretation function $\cdot^{\mcI_c}$. The domain consists of:

\begin{items} 
 \item Domain of objects $\Delta^{\mcI_c}_O = \{ c1, c2, c3, t1, t2, r1, r2, b1, b2 \}$, and
 \item Domain of values $\Delta^{\mcI_c}_V = \{ \textnormal{``Algebra I''}, \textnormal{``Economics I''}, \textnormal{``VO''}, \textnormal{``UE''},$ \\ 
 \hspace*{115pt} $\textnormal{``SEM1''}, \textnormal{``HS1''}, \textnormal{``Main''}, \textnormal{``Dep''} \}$.
\end{items}

\noindent The interpretation function $\cdot^{\mcI_c}$ maps all constant symbols in $\Gamma$ to the corresponding values in $\Delta^{\mcI_c}$, i.e.\ $e^{\mcI_c} = e$ for all $e \in \Gamma$. It is easily verified that this interpretation satisfies the KB $\mcK_c$, i.e. $\mcI_c \models \mcK_c$.\end{example}

\pagebreak 

\noindent We will now introduce the notion of an ABox seen as an interpretation, denoted by $\DB{\mcA}$.

\begin{definition}(ABox interpretation $\DB{\mcA}$ \cite{2009calvanese}) Let $\mcA$ be a $\DLA$ ABox. We denote by $\DB{A} = \left< \Delta^\DB{\mcA},\cdot^\DB{\mcA} \right>$ the interpretation defined as follows:
\begin{items}
 \item $\Delta^\DB{\mcA}$ is the non-empty set consisting of the union of the set of all object constant occurring in $\mcA$ and the set $\ffo{val}\left(c\right)$, such that $c$ is a value constant that occurs in  $\mcA$,
 \item $a^\DB{\mcA} = a$, for each object constant $a$,
 \item $A^\DB{\mcA} = \{ a \mid A\left(a\right) \in \mcA\}$, for each atomic concept $A$,
 \item $P^\DB{\mcA} = \{ \left(a_1,a_2\right) \mid P\left(a_1,a_2\right) \in \mcA\}$, for each atomic role $P$,
 \item $U^\DB{\mcA} = \{ \left(a, \ffo{val}\left(c\right)\right) \mid U\left(a,c\right) \in \mcA \}$, for each atomic attribute $U$.\qedhere
\end{items}
\end{definition}
\noindent It is clear that such an interpretation satisfies all ABox assertions, i.e.\ $\DB{\mcA} \models \mcA$. Notice that the interpretation $\mcI_c$ given in Example~\ref{ex:dl_int}, is exactly the ABox interpretation $\DB{\mcA_c}$, where $\mcA_c$ is the ABox given in Example~\ref{ex:dl_abox}.
\end{subsubsection}

\begin{subsubsection}{Queries over $\DLA$ KB}
We introduce here queries of $\DLA$ KBs. A first-order query $q$ over a $\DLA$ KB $\mcK$ is a, possibly open, first-order logic formula (FOL) $\varphi\left(\mathbf{x}\right)$. Such a query is built from atoms, which are in the case of queries over a $\DLA$ KB the following:
\begin{items}
 \item atomic concepts, written as $A\left(x\right)$,
 \item value-domains, written as $D\left(x\right)$,
 \item atomic roles, written as $P\left(x,y\right)$,
 \item atomic attributes, written as $U\left(x,y\right)$, or
 \item equality of variables, i.e.\ $x=y$.
\end{items}

\noindent The variables $x,y$ are either variables in $\mathbf{x}$ or constants in $\Gamma$. The free variables $\mathbf{x}$ of $\varphi\left(\mathbf{x}\right)$ form a tuple of (pairwise distinct) variables. The arity of a query is given by the arity of $\mathbf{x}$. A \emph{boolean query} is a query with arity $0$. We will only consider \textit{conjunctive} (CQ) and \textit{union of conjunctive} (UCQ) queries, which are of the form:
\begin{align*}
 q\left(\mathbf{x}\right) &\la \exists \mathbf{y}_1.\ffo{conj}_1\left(\mathbf{x},\mathbf{y}_1\right) \\
 & \vdots \\
 q\left(\mathbf{x}\right) &\la \exists \mathbf{y}_n.\ffo{conj}_n\left(\mathbf{x},\mathbf{y}_n\right)
\end{align*}

\noindent where $\ffo{conj}_k\left(\mathbf{x},\mathbf{y}_k\right)$ is a conjunction of atoms. The free variables $\mathbf{x}$ are also called \textit{distinguished} variables and the existentially quantified variables $y_1, \ldots, y_n$ are called \textit{non-distinguished} variables. A CQ is a UCQ with no disjunction. \\

\noindent Let $\mcI$ be an interpretation over a $\DLA$ KB. The answer to a UCQ $q = \varphi\left(\mathbf{x}\right)$ is the set $q^\mcI$ of tuples $\mathbf{o} = \Delta^\mcI \times \cdots \times \Delta^\mcI$ such that the formula $\varphi$ evaluates to true in $\mcI$ under the assignment that assigns each object in $\mathbf{o}$ to the corresponding variable in $\mathbf{x}$ \cite{2009calvanese}. The set of tuples $q^\mcI$ is called the answers to $q$ over $\mcI$. 

\begin{example}
Consider the KB from Example~\ref{ex:dl_abox} and let $\mcI_c$ be the interpretation given in Example~\ref{ex:dl_int}. The following query asks for the room and the type of a course:
$$q_1(r,l) \la \exists c.\rfo{is\_of\_type}\left(c,t\right) \wedge \rfo{located}\left(c,l\right).$$
\noindent The answers to $q_1$ are:
\begin{align*}
q_1^{\mcI_c} = \{ \left(r1,t1\right), \left(r2,t2\right) \}. & \qedhere
\end{align*}
\end{example}

\noindent The above notion of CQs only considers queries over a particular model of a KB. If we query a KB, we rather look for an answer over all possible interpretations. Such answers are called \textit{certain} and we define them as follows.

\begin{definition}{(Certain answers \cite{2009calvanese})}
Let $\mcK$ be a $\DLA$ KB and $q$ a UCQ over $\mcK$. A tuple $\mathbf{c}$ of constants appearing in $\mcK$ is a certain answer to $q$ over $\mcK$, written $\mathbf{c} \in \ffo{cert}\left(q,\mcK\right)$, if for every model $\mcI$ of $\mcK$, we have that $\mathbf{c}^\mcI \in q^\mcI$.
\end{definition}
\end{subsubsection}

\begin{subsubsection}{Reasoning in $\DLA$}
DLs provide different reasoning services. Among them, the most important, also for $\DLA$ KB, are \cite{2009calvanese}:
\begin{itemize}
 \item \textit{KB satisfiability}: Given a KB $\mcK$, verify whether $\mcK$ admits at least one model
 \item \textit{Concept and role satisfiability}: Given a TBox $\mcT$ and a concept $C$ (resp. a role $R$), verify whether $\mcT$ admits a model $\mcI$ such that $C^\mcI \neq \emptyset$ (resp. $R^\mcI \neq \emptyset$).
 \item \textit{Logical implication of an assertion}: A KB $\mcK$ logically implies an assertion $\alpha$, denote $\mcK \models \alpha$, if every model of $\mcK$ satisfies $\alpha$. Different types of assertions give different sub-problems: \textit{instance checking} ($\mcK \models C(a)$ or $\mcK \models R(a_1,a_2)$), \textit{subsumption of concepts or roles} ($\mcK \models C_1 \sqsubseteq C_2$ or $\mcK \models R_1 \sqsubseteq R_2$) or \textit{checking functionality} ($\mcK \models \funct{Q}$).
\end{itemize}


\noindent Notice that in $\DLA$ concept and role satisfiability, and logical implication of an assertion can be reduced to KB satisfiability (see \cite{2009calvanese} for details). Additionally, we are interested in:

\begin{itemize}
 \item \textit{Query answering}: Given a KB $\mcK$ and a query $q$ over $\mcK$, compute the set $\ffo{cert}\left(q,\mcK\right)$.
\end{itemize}

\end{subsubsection}
\end{subsection}

\begin{subsection}{Reasoning over $\DLA$ KB}
In DLs reasoning is an important task. We have presented several reasoning services, all of which, except of query answering, can be reduced to KB satisfiability. Therefore, we will provide an introduction to KB satisfiability in $\DLA$ as it is introduced in \cite{2009calvanese}. However, for the ease of presentation, we will make some simplifying assumptions. Those assumptions do not affect the generality of the presented results. First, we will not distinguish between concepts and values. Thus, our KBs contain only object constants, concepts and roles. Second, we will discard inclusion assertions of the form $B \sqsubseteq \top$. They do not have an impact on the semantics \cite{2009calvanese}.\\

\noindent We will define the notion of a \textit{canonical interpretation} of a $\DLA$ KB. Such an interpretation is constructed according to the notion of \textit{restricted chase} \cite{1984johnson, 1995databases}. This is done by first defining the notion of applicable assertions, then we define the chase for a $\DLA$ KB, and finally, we use the chase to define the canonical interpretation. In this thesis, we will make use of the following simplifying notation for a basic role $Q$ and two constants $a_1$, $a_2$:
\begin{align*}Q\left(a_1,a_2\right) \mbox{denotes} \begin{cases}
                                       P\left(a_1,a_2\right), & \mbox{if } Q=P, \\
                                       P\left(a_2,a_1\right), & \mbox{if } Q=P^-.
                                      \end{cases}\end{align*}
\begin{definition}{(Applicable PIs \cite{2009calvanese})} Let $\mcS$ be a set of $\DLA$ membership assertions. Then, a PI $\alpha$ is applicable in $\mcS$ to a membership assertion $\beta \in \mcS$ if
\begin{items}
 \item $\alpha = A_1 \sqsubseteq A_2$, $\beta = A_1(a)$, and $A_2(a) \notin \mcS$;
 \item $\alpha = A \sqsubseteq \exists Q$, $\beta = A(a)$, and there does not exist any constant $a^\prime$ such that $Q\left(a,a^\prime\right) \in \mcS$;
 \item $\alpha = \exists Q \sqsubseteq A$, $\beta = Q(a,a^\prime)$ for some $a^\prime$, and $A(a) \notin \mcS$;
 \item $\alpha = \exists Q_1 \sqsubseteq \exists Q_2$, $\beta = Q_1(a_1,a_2)$ for some $a_2$, and there does not exist any constant $a_2^\prime$ such that $Q_2(a_1,a_2^\prime) \in \mcS$;
 \item $\alpha = Q_1 \sqsubseteq Q_2$, $\beta = Q_1(a_1,a_2)$, and $Q_2(a_1,a_2) \notin \mcS$. \qedhere
\end{items}
\end{definition}


\noindent Applicable PIs can be used to extend a $\DLA$ model in order to satisfy all positive inclusion assertions of a $\DLA$ TBox. The chase consists of a possibly infinite number of chase steps. It starts with a $\DLA$ ABox $\mcA$. In each step a PI $\alpha$ is applied to a membership assertion $\beta$. Thus, we add a new membership assertion to $\mcA$, such that the PI $\alpha$ is not applicable to $\beta$ anymore. It is clear that this process strongly depends on the order of the applied PIs. We will assume the order to be fixed. This can be done by assuming an infinite set $\Gamma_N$ of lexicographically ordered constant symbols not occurring in $\mcA$ and a lexicographic ordering on the set of PIs. Now we can introduce the notion of the chase.

\begin{definition}{(The $\DLA$ chase \cite{2009calvanese})} Let $\mcK = \left< \mcT, \mcA \right>$ be a $\DLA$ KB, let $\mcT_p$ be the set of positive inclusion assertions in $\mcT$, let $n$ be the number of membership assertions in $\mcA$, and let $\Gamma_N$ be the set of lexicographically ordered constants not in $\mcA$. Assume that the membership assertions in $\mcA$ are numbered from 1 to $n$ following their lexicographic order, and consider the following definition of sets $\mcS_j$ of membership assertions:

\begin{items}
 \item $\mcS_0 = \mcA$
 \item $\mcS_{j+1} = \mcS_j \cup \{ \beta_{new} \}$, where $\beta_{new}$ is a membership assertion numbered with $n+j+1$ in $\mcS_{j+1}$ and obtained as follows:
 
 \begin{items}
    \item \textbf{let} $\beta$ be the first membership assertion in $\mcS_j$ such that there exists a PI $\alpha \in \mcT_p$ applicable in $\mcS_j$ to $\beta$
    \item \textbf{let} $\alpha$ be the lexicographically first PI applicable in $\mcS_j$ to $\beta$
    \item \textbf{let} $a_{new}$ be the constant of $\Gamma_N$ that follows lexicographically all constants in $\mcS_j$
    \item \textbf{case} $\alpha$, $\beta$ \textbf{of}
    
 \begin{tabular}{lllll}
   $\;$ & \textbf{(cr1)} & $\alpha = A_1 \sqsubseteq A_2$ & and $\beta = A_1(a)$ & \textbf{then} $\beta_{new} = A_2(a)$ \\
   $\;$ & \textbf{(cr2)} & $\alpha = A \sqsubseteq \exists Q$ & and $\beta = A(a)$ & \textbf{then} $\beta_{new} = Q(a,a_{new})$ \\
   $\;$ & \textbf{(cr3)} & $\alpha = \exists Q \sqsubseteq A$ & and $\beta = Q(a,a^\prime)$ & \textbf{then} $\beta_{new} = A(a)$ \\
   $\;$ & \textbf{(cr4)} & $\alpha = \exists Q_1 \sqsubseteq \exists Q_2$ & and $\beta = Q_1(a,a^\prime)$ & \textbf{then} $\beta_{new} = Q_2(a,a_{new})$ \\
   $\;$ & \textbf{(cr5)} & $\alpha = Q_1 \sqsubseteq Q_2$ & and $\beta = Q_1(a,a^\prime)$ & \textbf{then} $\beta_{new} = Q_2(a,a^\prime)$
 \end{tabular}
 \end{items}
\end{items}

 \noindent Then, we call chase of $\mcK$, denoted $\ffo{chase}\left({\mcK}\right)$, the set of membership assertions obtained by the infinite union of all $\mcS_j$, i.e.,
 
 \begin{align*}\ffo{chase}\left({\mcK}\right) = \bigcup_{j\in \mathbb{N}} \mcS_j. & \qedhere \end{align*}
\end{definition}

\noindent It is now possible to define the canonical interpretation of a $\DLA$ KB.

\begin{definition}{(Canonical interpretation ($\ffo{can}\left(\mcK\right)$))} The \textit{canonical interpretation} $\ffo{can}\left(\mcK\right) = \left< \Delta^{\ffo{can}\left(\mcK\right)}, \cdot^{\ffo{can}\left(\mcK\right)} \right>$ is the interpretation where:
\begin{items}
 \item $\Delta^{\ffo{can}\left(\mcK\right)} = \Gamma_O \cup \Gamma_N$,
 \item $a^{\ffo{can}\left(\mcK\right)} = a$, for each constant $a$ occurring in $\ffo{chase}\left(\mcK\right)$,
 \item $A^{\ffo{can}\left(\mcK\right)} = \{ a \mid A(a) \in \ffo{chase}\left(\mcK\right)\}$, for each atomic concept $A$, and
 \item $Q^{\ffo{can}\left(\mcK\right)} = \{ (a_1,a_2) \mid P(a_1,a_2) \in \ffo{chase}\left(\mcK\right)\}$, for each atomic role $P$. \qedhere
\end{items}
\end{definition}

\noindent The following property, proven in \cite{2009calvanese}, holds for $\ffo{can}\left(\mcK\right)$. 

\begin{lemma}{(Lemma 4.5 of \cite{2009calvanese})}
Let $\mcK = \left< \mcT, \mcA \right>$ be a $\DLA$ KB and let $\mcT_p$ be the set of positive inclusion assertions in $\mcT$. Then, $\ffo{can}\left(\mcK\right)$ is a model of $\left< \mcT_p, \mcA \right>$.
\end{lemma}

\noindent Since $\ffo{can}\left(\mcK\right)$ is a model of $\left< \mcT_p, \mcA \right>$, we can conclude that each KB, with only PIs in the TBox, is satisfiable. We now need to extend satisfiability to account for functional assertions and negative inclusion assertions. For functionality assertions satisfiability is easy to check. The following lemma says that we just need to verify if the interpretation $\DB{\mcA}$ satisfies the functionality assertions.

\begin{lemma}{(Lemma 4.6 of \cite{2006calvanese})} 
 Let $\mcK = \left< \mcT, \mcA \right>$ be a $\DLA$ KB, and let $\mcT_f$ be the set of functionality assertions in $\mcT$. Then, $\ffo{can}\left(\mcK\right)$ is a model of $\left< \mcT_f, \mcA \right>$ if and only if $\DB{\mcA}$ is a model of $\left< \mcT_f, \mcA \right>$.
\end{lemma}

\begin{proof}[Proof sketch] $\;$
\begin{items}
    \item[($\Ra$)] Follows from the fact that $\mcA \subseteq \ffo{chase}\left({\mcK}\right)$. 
    \item[($\La$)] In each chase step we choose an applicable PI $\alpha$. Only rules \textbf{cr2}, \textbf{cr4} and \textbf{cr5} can lead to a violation of a functionality assertion. Due to the restriction on $\DLA$ KBs, rule \textbf{cr5} cannot lead to a violation of a functional dependency. Assume the new constant $a_{new}$ introduced by rule \textbf{cr2} or \textbf{cr4} leads to a violation of a functionality assertion. This is only the case if there is a constant symbol $a^\prime$ such that $Q(a,a^\prime) \in \mcS$ or $Q_2(a,a^\prime) \in \mcS$. But then $\alpha$ would not have been applicable. Thus, the chase never introduces a violation of a functionality assertion. \qedhere
\end{items}
\end{proof}

\noindent We will now consider negative inclusion assertions. Ideally, we want to extend the previous lemma to negative inclusion assertions. But, it must not be the case that even if $\DB{\mcA}$ satisfies all NIs, $\ffo{can}\left(\mcK\right)$ may not satisfy them. This is due to an interaction between NIs and PIs. Consider, for example, the PI $A_1 \sqsubseteq A_2$ and the NI $A_2 \sqsubseteq \neg A_3$. These two inclusion assertions logically imply the NI $A_1 \sqsubseteq \neg A_3$. An ABox $\mcA$ might satisfy both inclusion assertions separately but violates the implied NI. This interaction is captured by closing the negative inclusion assertions with respect to the positive inclusion assertions as defined next.

\begin{definition}{(Closure of NIs $\ffo{cln}\left(\mcT\right)$ \cite{2009calvanese})}
Let $\mcT$ be a $\DLA$ TBox. We call \textit{NI-closure} of $\mcT$, denoted by $\ffo{cln}\left(\mcT\right)$, the TBox defined inductively as follows:
\begin{items}
 \item all functionality assertions in $\mcT$ are also in $\ffo{cln}\left(\mcT\right)$;
 \item all negative inclusion assertions in $\mcT$ are also in $\ffo{cln}\left(\mcT\right)$;
 \item if $B_1 \sqsubseteq B_2$ is in $\mcT$ and $B_2 \sqsubseteq \neg B_3$ or $B_3 \sqsubseteq \neg B_2$ is in $\ffo{cln}\left(\mcT\right)$, then also $B_1 \sqsubseteq \neg B_3$ is in $\ffo{cln}\left(\mcT\right)$;
 \item if $Q_1 \sqsubseteq Q_2$ is in $\mcT$ and $\exists Q_2 \sqsubseteq \neg B$ or $B \sqsubseteq \neg \exists Q_2$ is in $\ffo{cln}\left(\mcT\right)$, then also $\exists Q_1 \sqsubseteq \neg B$ is in $\ffo{cln}\left(\mcT\right)$;
 \item if $Q_1 \sqsubseteq Q_2$ is in $\mcT$ and $\exists Q_2^- \sqsubseteq \neg B$ or $B \sqsubseteq \neg \exists Q_2^-$ is in $\ffo{cln}\left(\mcT\right)$, then also $\exists Q_1^- \sqsubseteq \neg B$ is in $\ffo{cln}\left(\mcT\right)$;
 \item if $Q_1 \sqsubseteq Q_2$ is in $\mcT$ and $Q_2 \sqsubseteq \neg Q_3$ or $Q_3 \sqsubseteq \neg Q_2$ is in $\ffo{cln}\left(\mcT\right)$, then also $Q_1 \sqsubseteq \neg Q_3$ is in $\ffo{cln}\left(\mcT\right)$;
 \item if one of the assertions $\exists Q \sqsubseteq \neg \exists Q$, $\exists Q^- \sqsubseteq \neg \exists Q^-$, or $Q \sqsubseteq \neg Q$ is in $\ffo{cln}\left(\mcT\right)$, then all three such assertions are in $\ffo{cln}\left(\mcT\right)$. \qedhere
\end{items}
\end{definition}

\noindent Notice that $\ffo{cln}\left(\mcT\right)$ does not imply new negative inclusion assertions or functionality assertions not implied by $\mcT$. The next lemma, proven in \cite{2009calvanese}, shows that we can use the ABox minimal model to check satisfiability of negative inclusions.

\begin{lemma}{(Lemma 4.9 from \cite{2009calvanese})} Let $\mcK = \left< \mcT, \mcA \right>$ be a $\DLA$ KB. Then, $\ffo{can}\left(\mcK\right)$ is a model of $\mcK$ if and only if $\DB{\mcA}$ is a model of $\left<\ffo{cln}\left(\mcT\right),\mcA\right>$.\end{lemma}

\noindent Now that we can check satisfiability of functionality and negative inclusion assertions we need to establish satisfiability of a $\DLA$ KB. A $\DLA$ KB $\mcK$ is satisfiable if $\ffo{can}\left(\mcK\right)$ is a model of $\mcK$ and vice versa (see Lemma 4.11 of \cite{2009calvanese}). Unfortunately, the construction of $\ffo{can}\left(\mcK\right)$ might not be convenient or even possible. If we combine the previous observations, we can show that satisfiability of a KB can be checked by looking at $\DB{\mcA}$. This is captured by the following theorem, which follows from the previous established observations and lemmas.

\begin{theorem}{(Theorem 4.12 from \cite{2009calvanese})} Let $\mcK = \left< \mcT, \mcA \right>$ be a $\DLA$ KB. Then, $\mcK$ is satisfiable if and only if $\DB{\mcA}$ is a model of $\left<\ffo{cln}\left(\mcT\right),\mcA\right>$.
\end{theorem}

\noindent We can verify whether $\DB{\mcA}$ is a model of $\left<\ffo{cln}\left(\mcT\right),\mcA\right>$ by evaluating a suitable boolean UCQ with inequalities over $\DB{A}$. We define such a boolean UCQ via a translation $\delta$ from the assertions in $\ffo{cln}\left(\mcT\right)$ as follows \cite{2009calvanese}:
\begin{align*}
 \delta\left(\funct{P}\right) &= \exists x,y_1,y_2.P\left(x,y_1\right) \wedge P\left(x,y_2\right) \wedge y_1 \neq y_2 \\
 \delta\left(\funct{P^-}\right) &= \exists x_1,x_2,y.P\left(x_1,y\right) \wedge P\left(x_2,y\right) \wedge x_1 \neq x_2 \\
 \delta\left(B_1 \sqsubseteq \neg B_2\right) &= \exists x.\gamma_1\left(B_1,x\right)\wedge \gamma_2 \left(B_2,x\right) \\
 \delta\left(Q_1 \sqsubseteq \neg Q_2\right) &= \exists x,y.Q_1\left(x,y\right)\wedge Q_2\left(x,y\right)
\end{align*}
\noindent where in the last two equations
\begin{align*}
 \gamma_i\left(B,x\right) &= \begin{cases}
                             A\left(x\right), & \mbox{if } B = A, \\
                             \exists y_i.P\left(x,y_i\right), & \mbox{if } B = \exists P, \\
                             \exists y_i.P\left(y_i,x\right), & \mbox{if } B = \exists P^-,
                             \end{cases} 
\end{align*}

\noindent Notice that the queries ask for a violation of an assertion. Therefore, if the evaluation of the UCQ $$\bigcup_{\alpha \in \ffo{cln}\left(\mcT\right)} \delta(\alpha)$$ over $\DB{\mcA}$ returns the empty set then $\mcK$ is satisfiable (see Lemma 4.13 of \cite{2009calvanese}). Hence, KB satisfiability in $\DLA$ can be reduced to query evaluation over a database. 
\end{subsection}

\begin{subsection}{Universal Model}
 In the previous section we have established the notion of the $\DLA$ chase and as a result we have defined the canonical interpretation $\ffo{can}\left(\mcK\right)$. The question is, whether such an interpretation is a representation of all possible interpretations of $\mcK$. Such an interpretation is called a \emph{universal model}. We will show that $\ffo{can}\left(\mcK\right)$ is indeed a universal model. But first, we need to define universal models. These are defined in terms of homomorphisms as follows.
 
 \pagebreak 
 
 \begin{definition}
  Let $\mcK$ be a $\DLA$ KBs; $\mfo{I}$ and $\mfo{J}$ be interpretations of the KB.
  \begin{itemize}
   \item[1.] A \emph{homomorphisms} $h : \mfo{I} \ra \ifo{J}$ is a mapping from $\Delta^\mfo{I}$ to $\Delta^\mfo{J}$ such that: 
   \begin{items}
    \item[(i)] for all $a \in \Delta^\mfo{I}$ and for each atomic concept $C \in \ffo{concepts}\left(\mcK\right)$: if $a \in C^\mfo{I}$ then $h\left(a\right) \in C^\mfo{J}$,
    \item[(ii)] for all $(a,b) \in \Delta^\mfo{I} \times \Delta^\mfo{J}$ and for each atomic role $P \in \ffo{roles}\left(\mcK\right)$: if $\left(a,b\right) \in P^\mfo{I}$ then $\left(h\left(a\right),h\left(b\right)\right) \in P^\mfo{J}$.
   \end{items}
   \item[2.] $\mfo{I}$ is \emph{homomorphically equivalent} to $\mfo{J}$ if there is a homomorphism $h: \mfo{I} \ra \mfo{J}$ and a homomorphism $h^\prime: \mfo{J} \ra \mfo{I}$. \qedhere
  \end{itemize}
 \end{definition}
 
\begin{definition}{(Universal model \cite{2006kharlamov, 1995databases})} Let $\mcK$ be a $\DLA$ KB. A universal model for $\mcK$ is a model $\mcU \models \mcK$ such that for every model $\mcI \models \mcK$, there exists a homomorphism $h : \Delta^\mcU \ra \Delta^\mcI$.
\end{definition}

\noindent With this definition we can show that $\ffo{can}\left(\mcK\right)$ is indeed a universal model for $\mcK$.

\begin{theorem}{(Theorem 4 of \cite{2006kharlamov})}
 Let $\mcK$ be a $\DLA$ KB. If $\mcK$ is satisfiable, then $\ffo{can}\left(\mcK\right)$ is a universal model for $\mcK$.
\end{theorem}

\begin{proof}[Proof idea.] Since $\mcK$ is satisfiable, $\ffo{can}\left(\mcK\right)$ is a model of $\mcK$. It remains to show that for any model $\mcI$ of $\mcK$ it holds that there exists a homomorphism from  $\ffo{can}\left(\mcK\right)$ to $\mcI$. It is easy to see, that for each model $\mcI$ of $\mcK$ it holds that there is a homomorphism $h$ from $\DB{\mcA}$ to $\mcI$. As we extend the interpretation in each chase step, we can extend the homomorphism $h$ in each chase step to the (possible) new introduced constants, resulting in a homomorphism $h^\prime$. Finally, at the end of the chase, we have constructed a homomorphism from $\ffo{can}\left(\mcK\right)$ to $\mcI$, which proves that $\ffo{can}\left(\mcK\right)$ is a universal model of $\mcK$.
\end{proof}
 
\end{subsection}

\begin{subsection}{Query Answering over finite interpretations}
  Query answering in $\DLA$ is an important task. Several methods for query answering in $\DLA$ KBs exist. It is possible to evaluate a query over the canonical model of the KB (see Theorem 6 and Corollary 3 of \cite{2006kharlamov}). The drawback of this method is that the canonical model might be infinite. In this section we will show a syntactic criterion that ensures a finite chase. We will present sets of \emph{weakly-acyclic positive inclusion assertions}, which are a DL version of \emph{weakly-acyclic tuple-generating dependencies} introduced by Fagin et al.\ \cite{2005fagin}. We can show that any chase of a KB with weakly-acyclic PIs is polynomial in the size of the KB. \\
  
  \noindent Let $\mcK$ be a $\DLA$ KB. We denote with $B_\mcK$ the set of all basic concepts occurring in $\mcK$. The set $B_\mcK$ consists of atomic concepts and concepts of the form $\exists R$ or $\exists R^-$, where are $R$ is an atomic role. A \emph{dependency graph} is defined as follows.
  
  \begin{definition}{(Dependency graph \cite{2006kharlamov})}
     Let $\mcK$ be a $\DLA$ KB. A dependency graph for $\mcK$, denoted as $G_\mcK$, is a directed edge-labeled graph, such that:
     \begin{items}
      \item[1.] the set of nodes of $G_\mcK$ is $B_\mcK$;
      \item[2.] the set of non-labeled edges of $G_\mcK$ is defined as follows: 
      \begin{items}
         \item[(a)] For every PI $B \sqsubseteq B^\prime$ in $\mcK$, where $B$ and $B^\prime$ are basic concepts, there is a non-labeled edge from $B$ to $B^\prime$, denoted by $B \longrightarrow B^\prime$.
         \item[(b)] For every PI $Q_1 \sqsubseteq Q_2$ in $\mcK$, where $Q_1$ and $Q_2$ are basic roles, there are non-labeled edges $\exists Q_1 \longrightarrow \exists Q_2$ and $\exists Q_1^- \longrightarrow \exists Q_2^-$.
     \end{items}
     \item[3.] the set of $*$-labeled edges of $B_\mcK$ is defined as follows: Let $B$ and $B^\prime$ be two nodes in $G_\mcK$. If it holds that
     \begin{items} 
        \item[(a)] there is an edge $B \longrightarrow B^\prime$,
        \item[(b)] $B^\prime = \exists R$ or $B^\prime = \exists R^\prime$, and
        \item[(c)] $\exists R^- \in B_\mcK$ or $\exists R \in B_\mcK$ respectively,
     \end{items}
     \noindent then there is a $*$-labeled edge $B \longrightarrow^* \exists R^-$ or $B \longrightarrow^* \exists R$ in $G_\mcK$. \qedhere
     \end{items}
  \end{definition}

  \begin{definition}{(Weak-acyclicity)} A set of PIs is \emph{weakly-acyclic} if its dependency graph has no cycles that contain a $*$-labeled edge. A KB is weakly-acyclic if the set of all its inclusion assertions is weakly-acyclic.
  \end{definition}
  
  \begin{example}
   Let us consider the $\DLA$ KB $\mcK^\prime$ consisting of the following set of PIs:
   \begin{align*}
      B & \sqsubseteq \exists R & A & \sqsubseteq \exists Q^- & \exists R^- & \sqsubseteq A & Q^- & \sqsubseteq R
   \end{align*}
   
   \noindent The dependency graph consists of the nodes $B_\mcK = \{ A, B, \exists R, \exists R^-, \exists Q, \exists Q^- \}$ and is depicted in Figure~\ref{fig:depGraph}.
   
   \begin{figure}[t]
   \begin{center}
   \input{figures/dl/dep_graph.tikz} 
   \end{center}
   \caption{A dependency graph $G_{\mcK^\prime}$ with a cycle (in \textcolor{red}{red}) that contains a $*$-labeled edge } 
   \label{fig:depGraph}
   \end{figure}

   \noindent Since the dependency graph has a cycle that contains a $*$-labeled edge, the KB $\mcK^\prime$ is not weakly-acyclic.
  \end{example}

  \noindent The intuition of a dependency graph is that each non-labeled edge keeps track of the fact that a constant may be propagated during the chase from the concept at the origin to the concept at the end of the edge. Edges labeled with a $*$ keep track of newly introduced constants. If now a cycle goes through a labeled edge, then the newly introduced constant introduces again another new constant at a later chase step. Therefore, the chase continues forever and leads to an infinite interpretation. It is possible to show the following:
  
  \begin{theorem}{(Theorem 7 in \cite{2006kharlamov})}
   For a satisfiable weakly-acyclic $\DLA$ KB its chase has depth which is polynomial in the size of the KB.
  \end{theorem}
  
  \begin{proof}The proof is similar to the proof of Theorem 3.9 in \cite{2005fagin}.\end{proof}

  \noindent It immediately follows that for a satisfiable weakly-acyclic $\DLA$ KB, we can compute the chase and evaluate any query over the canonical model.
\end{subsection}



\begin{subsection}{Query Answering over infinite interpretations}
 A more general method for query answering was introduced in \cite{2009calvanese}. This method separates the intensional and extensional level of the $\DLA$ KB. First, the query is processed and reformulated based on the assertions in the TBox. Then, the reformulated query is evaluated over the ABox. This is similar to the presented method for KB satisfiability.
 
 \begin{subsubsection}{Query Reformulation} 
 We are going to present the query reformulation algorithm as introduced in \cite{2009calvanese}. First, we define some preliminary notions. We distinguish between \textit{bound} and \textit{unbound} arguments of an atom in a query. Bound variables correspond to distinguished or shared variables, which are variables that either occur at least twice in the queries body or are a constant. The other variables are called unbound. The symbol '$\_$' is used to represent non-distinguished non-shared, i.e.\ unbound, variables. 
 
 Next we define when a PI is applicable to an atom $g$ \cite{2009calvanese}:
 
 \begin{items}
  \item A PI $\alpha$ is applicable to an atom $A\left(x\right)$, if $\alpha$ has $A$ in its right-hand side.
  \item A PI $\alpha$ is applicable to an atom $P\left(x_1,x_2\right)$, if one of the following conditions holds:
  \begin{items}
      \item[(i)] $x_2 = \_$ and the right-hand side of $\alpha$ is $\exists P$; or
      \item[(ii)] $x_1 = \_$ and the right-hand side of $\alpha$ is $\exists P^-$; or
      \item[(iii)] $\alpha$ is a role inclusion assertion and its right-hand side is either $P$ or $P^-$.
  \end{items}
 \end{items}
 
\noindent The function $gr\left(g,\alpha\right)$ returns the atom obtained from $g$ by applying the applicable inclusion $\alpha$ as defined by the following table:

\begin{table}[h]
 \centering
 \begin{tabular}{l|c|l}
    \multicolumn{1}{c|}{Atom $g$} & Positive inclusion $\alpha$ & \multicolumn{1}{c}{$gr(g,\alpha)$} \\
    \hline $A(x)$ & $A_1 \sqsubseteq A$ & $A_1(x)$ \\
    $A(x)$ & $\exists Q \sqsubseteq A$ & $Q(x,\_)$ \\
    $Q(x,\_)$ & $A \sqsubseteq \exists Q$ & $A(x)$ \\
    $Q(x,\_)$ & $\exists Q_1 \sqsubseteq \exists Q$ & $Q_1(x,\_)$ \\
    $Q(x_1,x_2)$ & $Q_1 \sqsubseteq Q$ & $Q_1(x_1,x_2)$ \\
 \end{tabular}
 \caption{The result $gr(g,\alpha)$ of applying a positive inclusion $\alpha$ to an atom $g$ (Fig. 12 adapted from \cite{2009calvanese})}
 \label{tag:gr}
\end{table}

\noindent The algorithm \textsf{PerfectRef}, given as Algorithm~\ref{alg:dl_perfectref}, reformulates a UCQ by taking into account the PIs of a TBox $\mcT$. As a first step (line 5 of Algorithm~\ref{alg:dl_perfectref}), the algorithm reformulates the atoms of each CQ $g^\prime \in q^\prime$, and produces a new query for each atom reformulation. This is denoted by $q^\prime\left[g / gr\left(g,\alpha\right)\right]$, which means that we replace in $q^\prime$ each atom $g$ with a new atom $g^\prime$, obtained by $gr\left(g,\alpha\right)$. As a second step (line 12 of Algorithm~\ref{alg:dl_perfectref}), we look for pairs of atoms $g_1$ and $g_2$ that unify. The function \textit{reduce} then returns a new CQ by applying the most general unifier to the atoms $g_1$ and $g_2$. Therefore, variables that are bound may become unbound in the new CQ. The function \textit{anon} then replaces each unbound variable by the symbol '$\_$'. 

\noindent Notice that the reformulation only depends on the PIs of a $\DLA$ TBox. Actually it is the case that once we have established KB satisfiability, we can discard NIs and functionality assertions for query answering. It has been shown that the algorithm \textsf{PerfectRef} terminates \cite{2009calvanese}.

 \begin{algorithm}[t]
 \SetKwInOut{Input}{input}
\SetKwInOut{Output}{output}

\Input{UCQ $q$, $\DLA$ TBox $\mcT$}
\Output{UCQ $pr$}

\BlankLine

 $pr \la q$\;
 \Repeat{$pr^\prime = pr$}{
    $pr^\prime \la pr$\;
    \ForEach{CQ $q^\prime \in pr^\prime$}{
       \ForEach{atom $g$ in $q^\prime$}{
          \ForEach{PI $\alpha$ in $\mcT$}{
             \If{$\alpha$ is applicable to $g$}{
                $pr \la pr \cup \{ q^\prime\left[g / gr\left(g,\alpha\right)\right] \}$\;
             }
          }
       }
       \ForEach{pair of atoms $g_1,g_2$ in $q^\prime$}{
          \If{$g_1$ and $g_2$ unify}{
             $pr \la pr \cup \{ \ffo{anon}\left(\ffo{reduce}\left(q^\prime,g_1,g_2\right)\right)\}$\;
          }
       }
    }
 }
 \Return{pr}
 \BlankLine
 \caption{The algorithm \textsf{PerfectRef} that computes the perfect reformulation of a CQ w.r.t. a $\DLA$ TBox (Fig. 13 from \cite{2009calvanese})}
 \label{alg:dl_perfectref} 
 \end{algorithm}

\begin{example}
\label{ex:perfect_ref}
Consider the $\DLA$ TBox $\mcT_c$ given in Example~\ref{ex:dl_tbox}. Now consider the CQ $q$ over $\mcT_c$:
$$q(x) \la \rfo{located}\left(x,y\right), \rfo{has\_room}\left(\_,y\right),$$
which queries for courses that are located in a room that belongs to a building. We will go through the steps of the algorithm \textsf{PerfectRef}$\left(\{q\},\mcT_c\right)$. In the first iteration the algorithm applies to the atom $has\_room\left(\_,y\right)$ the PI $room \sqsubseteq \exists has\_room^-$ and adds to $pr$ the new query:
$$q(x) \la \rfo{located}\left(x,y\right), \rfo{room}\left(y\right).$$
\noindent In the next iteration, the PI $\exists located^- \sqsubseteq room$ is applied to the atom $room(y)$ and the following query is inserted in $pr$:
$$q(x) \la \rfo{located}\left(x,y\right), \rfo{located}\left(\_,y\right).$$
\noindent Notice that there are now two atoms $\rfo{located}\left(x,y\right)$ and $\rfo{located}\left(\_,y\right)$ that can be unified. The function $\ffo{reduce}\left(q, \rfo{located}\left(x,y\right), \rfo{located}\left(\_,y\right)\right)$ returns the atom $\rfo{located}\left(x,y\right)$. Since $y$ is unbound, the function $\ffo{anon}$ replaces $y$ by $\_$. Therefore, the algorithm inserts in $pr$ the new query:
$$q(x) \la \rfo{located}\left(x,\_\right).$$
\noindent In the next iteration, it is, due to unification, possible to apply the PI $course \sqsubseteq \exists located$ to $\rfo{located}\left(x,\_\right)$. This inserts in $pr$ the new query
$$q(x) \la \rfo{course}\left(x\right).$$
\noindent At a further iteration, the algorithm applies the PI $\exists is\_of\_type \sqsubseteq course$ to $course(x)$ and adds to $pr$ the new query
$$q(x) \la \rfo{is\_of\_type}\left(x,\_\right).$$
\noindent Finally, the set of the five queries from above and the original query is returned by the algorithm \textsf{PerfectRef}$\left(\{q\},\mcT_c\right)$. 
\end{example}

\noindent Given that a $\DLA$ KB $\mcK$ is satisfiable, the query returned by \textsf{PerfectRef} can be evaluated over the ABox $\mcA$ considered as a relational database, denoted by $\DB{\mcA}$. The returned answers are correct and coincide with the certain answers $\ffo{cert}\left(q,\mcK\right)$ (see Theorem 5.14 of \cite{2009calvanese}). The query returned by \textsf{PerfectRef}$\left(\{q\},\mcT\right)$ is called the \emph{perfect rewriting} of $q$.
\end{subsubsection}
\end{subsection}



\begin{subsection}{Additional Notions}

In this section we further need the notion of isomorphisms and bisimulations as defined as follows. Isomorphisms and bisimulations help us to establish a relationship between two structures, which are in our case $\DLA$ interpretations.

\begin{definition}{(Isomorphism)}
Let $\mfo{I}$ and $\mfo{J}$ be two models of a $\DLA$ KB. $\mfo{I}$ and $\mfo{J}$ are \textit{isomorphic} denoted as $\mfo{I} \cong \mfo{J}$ if there exists a bijective function $h : \Delta^\mfo{I} \ra \Delta^\mfo{J}$, s.t.
\begin{itemize}
 \item for all $a \in \Delta^\mfo{I}$ and for each atomic concept $C \in \ffo{concepts}(\mcT)$: $a \in C^\mfo{I}$ if and only if $\left(a^\mfo{I}\right) \in C^\mfo{J}$, and
 \item for all $\left(a,b\right) \in \Delta^\mfo{I} \times \Delta^\mfo{I}$ and for each atomic role $R \in \ffo{roles}(\mcT)$: $\left(a^\mfo{I},b^\mfo{I}\right) \in R^\mfo{I}$ if and only if $\left(h\left(a^\mfo{I}\right),h\left(b^\mfo{I}\right)\right) \in P^\mfo{J}$. \qedhere
\end{itemize}
\end{definition}

\noindent Notice that an isomorphism is a bijective homomorphism.

\begin{definition}{(Bisimulation (adapted to $\DLA$ from \cite{2012sangiorgi}))}
\label{def:bisim}
A bisimulation $\sim_\mcB$ between two $\DLA$ interpretations $\mfo{I}$ and $\mfo{J}$ is a relation in $\Delta^\mfo{I} \times \Delta^\mfo{J}$ such that, for every pair of objects $o_1 \in \Delta^\mfo{I}$ and $o_2 \in \Delta^\mfo{J}$, if $o_1 \sim_\mcB o_2$ then the following hold:
\begin{itemize}
 \item for every atomic concept $A$: $o_1 \in A^\mfo{I}$ if and only if $o_2 \in A^\mfo{J}$;
 \item for every atomic role $P$:
 \begin{itemize}
  \item for each $o^\prime_1$ with $\left( o_1, o^\prime_1\right) \in P^\mfo{I}$, there is an $o^\prime_2$ with $\left( o_2, o^\prime_2 \right) \in P^\mfo{J}$ such that $o^\prime_1 \sim_\mcB o^\prime_2$;
  \item for each $o^\prime_2$ with $\left( o_2, o^\prime_2\right) \in P^\mfo{J}$, there is an $o^\prime_1$ with $\left( o_1, o^\prime_1 \right) \in P^\mfo{I}$ such that $o^\prime_1 \sim_\mcB o^\prime_2$;
 \end{itemize}
 \item for every atomic role $P$ (inverse property):
 \begin{itemize}
  \item for each $o^\prime_1$ with $\left( o^\prime_1, o_1\right) \in P^\mfo{I}$, there is an $o^\prime_2$ with $\left( o^\prime_2, o_2 \right) \in P^\mfo{J}$ such that $o^\prime_1 \sim_\mcB o^\prime_2$;
  \item for each $o^\prime_2$ with $\left( o^\prime_2, o_2\right) \in P^\mfo{J}$, there is an $o^\prime_1$ with $\left( o^\prime_1, o_1 \right) \in P^\mfo{I}$ such that $o^\prime_1 \sim_\mcB o^\prime_2$;\qedhere
 \end{itemize}
\end{itemize}
\end{definition}

\noindent Let $\pi$, $\pi^\prime$ be two sets of objects, such that $\pi \subseteq \Delta^\mfo{I}$ and $\pi^\prime \subseteq \Delta^\mfo{J}$. We say $\pi$ bisimulates $\pi^\prime$, denoted by $\pi \sim_\mcB \pi^\prime$, if every object $o \in \pi$ bisimulates every object in $\pi^\prime$ and vice versa. That is, for every $o \in \pi$, it holds that $o \sim_\mcB o^\prime$ for all $o^\prime \in \pi^\prime$ and for every $o^\prime \in \pi^\prime$, it holds that $o \sim_\mcB o^\prime$ for all $o \in \pi$.
\end{subsection}

\end{section}

\begin{section}{A Direct Mapping of Relational Data to Description Logic Knowledge Bases}
\label{sec:dl_map}

In this section we will show how to map relational data to $\DLA$ KBs. First, we will review the direct mapping of relational data to RDF as presented by the W3C \cite{2012rdbmapping} and Sequeda et al.\ \cite{2012Sequeda}. We will discuss their weaknesses regarding the lack of means to capture all semantic information of the relational model. We will therefore introduce a direct mapping of relational data to $\DLA$ knowledge bases that overcomes the limitations of the previous translations.

\begin{subsection}{A Direct Mapping of Relational Data to RDF}
 Most of the data in information systems is stored in relational databases. It is important for the success of the Semantic Web to utilize the information stored in relational databases. Therefore an automatic translation of relational data to RDF is needed. The W3C consortium introduced such a translation, called ``A Direct Mapping of Relational Data to RDF'' (RDB-direct-mapping) \cite{2012rdbmapping}. This direct mapping defines an RDF graph representation of the data in a relational database. Such an RDF graph can then be further processed, for example it can be queried using an RDF query language or it can be merged with other RDF graphs to add further information to the information specified in a relational table. \\
 
 \noindent The RDB-direct-mapping specifies that a relational database is translated into an RDF graph, which is called \textit{direct graph}. Such a direct graph is the union of the \textit{table graphs} for each table in a relational schema. A table graph is the union of \textit{row graphs} for each row in a table. A row graph is an RDF representation of a row of a relational table. Each row is identified by a \textit{row node}. The row node has as name, its table's name and the values of all primary key columns, for example \texttt{course/lecture=AlgebraI;type=VO}. If a table does not have a primary key, then a fresh blank node is used as a row node. For each row of a table, the row graph consists of the following:
 
 \begin{itemize}
  \item A \textit{row type triple} which specifies the type (table) of a row node (see number 4.1, 4.6 and 4.11 in Figure~\ref{fig:RDFCourse}).
  \item \textit{Reference triples} represent the foreign keys of a table. For this a special predicate is used. This predicate's label consists of the tables name, the keyword \texttt{ref} and the columns name, for example \texttt{course\#ref-room} (see numbers 4.2, 4.7 and 4.12 in Figure~\ref{fig:RDFCourse}).
  \item \textit{Literal triples} store the value of the row's columns. The predicate that is used for literal triples contains the table's name and the column's name, for example \texttt{course\#room} (see numbers 4.3-4.5, 4.8-4.10 and 4.13-4.15 in Figure~\ref{fig:RDFCourse}). 
 \end{itemize}
 \begin{figure}[t]
 \small
 \begin{align}
& \left(\texttt{course/lecture=AlgebraI;type=VO},\texttt{rdf:type},\cfo{course}\right) \\ 
& \textcolor{red}{\left(\texttt{course/lecture=AlgebraI;type=VO},\texttt{course\#ref-room},\texttt{rooms/room=HS1}\right)} \\
& \left(\texttt{course/lecture=AlgebraI;type=VO},\texttt{course\#lecture},\mbox{``Algebra I''}\right) \\
& \left(\texttt{course/lecture=AlgebraI;type=VO},\texttt{course\#type},\mbox{``VO''}\right) \\
& \textcolor{red}{\left(\texttt{course/lecture=AlgebraI;type=VO},\texttt{course\#room},\mbox{``HS1''}\right)} \\ 
& \left(\texttt{course/lecture=AlgebraI;type=UE},\texttt{rdf:type},\cfo{course}\right) \\
& \textcolor{red}{\left(\texttt{course/lecture=AlgebraI;type=UE},\texttt{course\#ref-room},\texttt{rooms/room=SEM1}\right)} \\
& \left(\texttt{course/lecture=AlgebraI;type=UE},\texttt{course\#lecture},\mbox{``Algebra I''}\right) \\
& \left(\texttt{course/lecture=AlgebraI;type=UE},\texttt{course\#type},\mbox{``UE''}\right) \\
& \textcolor{red}{\left(\texttt{course/lecture=AlgebraI;type=UE},\texttt{course\#room},\mbox{``SEM1''}\right)} \\ 
& \left(\texttt{course/lecture=EconomicsI;type=UE},\texttt{rdf:type},\cfo{course}\right) \\ 
& \textcolor{red}{\left(\texttt{course/lecture=EconomicsI;type=UE},\texttt{course\#ref-room}, \texttt{rooms/room=SEM1}\right)} \\
& \left(\texttt{course/lecture=EconomicsI;type=UE},\texttt{course\#lecture},\mbox{``Economics I''}\right) \\
& \left(\texttt{course/lecture=EconomicsI;type=UE},\texttt{course\#type},\mbox{``UE''}\right) \\ 
& \textcolor{red}{\left(\texttt{course/lecture=EconomicsI;type=UE},\texttt{course\#room},\mbox{``SEM1''}\right)}
 \end{align}
 \caption{The RDF triples obtained by the RDB-direct-mapping \cite{2012rdbmapping} from the relational table in Figure~\ref{fig:relCourse3NF}. In \textcolor{red}{red} are the triples that are in the result of the RDB-direct-mapping but not in the result of the direct mapping $\mcD\mcM$ \cite{2012Sequeda}, which will be introduced next.} 
 \label{fig:RDFCourse}
 \end{figure}
 
\noindent The RDB-direct-mapping does not add any further information on the semantics of the data in the relational database. This allows to specify information that cannot be present in any relational database. Consider for example the triple $$\left(\texttt{course/lecture=AlgebraI;type=VO},\texttt{rdf:type},\cfo{rooms}\right),$$ which extends the RDF triples given in Figure~\ref{fig:RDFCourse}. Such a triple would infer that the row, which is identified by the row node \texttt{course/lecture=AlgebraI;type=VO} is also a row in the ``rooms'' table. But, the relational model does not allow for rows that belong to different tables. Hence, the RDB-direct-mapping does not preserve the semantics of the relational model.\\

\noindent For a direct mapping $\mcM$ it would be desirable to preserve the semantics of the relational model. Additionally, a direct mapping should have other fundamental and desirable properties. These are introduced in \cite{2012Sequeda} and are defined as follows:

\begin{paragraph}{Fundamental properties}
  \begin{items}
  \item \textit{Information preservation} guarantees that the mapping does not loose any information. Formally, a direct mapping is information preserving if we can define a computable function $\mcN$, such that $\mcN$ translates RDF graphs to instances of a relational schema $R$. Additionally, the result of $\mcN$, applied to an RDF graph directly mapped from an instance $\ifo{I}$ of a relational schema, should return the same instance $\ifo{I}$, i.e.\ $\mcN\left(\mcM\left(R,\ifo{I}\right)\right) = \ifo{I}$. 
  \item \textit{Query preservation} guarantees that everything that can be extracted from a relational database, can also be extracted from the translated RDF graph via a suitable query language. That is, we can translate queries over the relational database into equivalent queries over RDF graphs.
 \end{items}
 
 \noindent Notice that neither of the two properties includes the other. Thus, we can have a direct mapping that preserves information, but maps this information such that a more powerful query language has to be used. On the other side, if, for example, the instances are mapped, but not the schema, it might be the case that the mapping is query preserving but not information preserving. 
\end{paragraph}
\begin{paragraph}{Desirable properties}
 \begin{itemize}
  \item \textit{Monotonicity}: Let $I_1$ and $I_2$ be instances of a relational schema, such that $I_1$ is contained in $I_2$. Then a direct mapping is monotone, if the direct mapping of $I_2$ is contained in $I_1$. Therefore, with a monotone direct mapping whenever we add new data to the relational database, we only have to map the new data and not the whole database.
  \item \textit{Semantics preservation} guarantees that data dependencies are encoded in the translation process. Let $\ifo{I}$ be an instance of a relational schema $R$ and $\Sigma$ a set of data dependencies. Then, a direct mapping $\mcM$ is called semantics preserving, if $I \models \Sigma$ if and only if $\mcM\left(R,I\right)$ is a model of the translated data dependencies.
 \end{itemize}
\end{paragraph}

\noindent The direct mapping $\mcD\mcM$ introduced by Sequeda et al.\ \cite{2012Sequeda} extends the RDB-direct-mapping in such a way that it is information and query preserving. $\mcD\mcM$ translates the relational schema and the relational instances via Datalog rules into an RDF graph. This process is similar to the direct mapping introduced previously. We will present here the differences from the RDB-direct-mapping. Additionally, for the ease of presentation, we will ignore the fact that the direct mapping $\mcD\mcM$ reverse engineers binary relations that result from modeling $n:m$-relationships of the conceptual model. Therefore, we will discuss the direct mapping from a database consisting of a single relation, and compare the result with the result from the RDB-direct-mapping depicted in Figure~\ref{fig:RDFCourse}. The direct mapping $\mcD\mcM$ translates a relational schema $R[A_1,\ldots,A_n]$ as follows: \\

\noindent \textbf{Relational instances} are translated as in the RDB-direct-mapping, except:
 \begin{items}
     \item Columns that are foreign keys directly refer to the row node of the referenced table. We do not store a tuple with a predicate having the ``\#ref'' keyword. For example, in Figure~\ref{fig:RDF2Course} triples numbered 4.27, 4.31 and 4.35 are added, and the triples drawn in \textcolor{red}{red} of Figure~\ref{fig:RDFCourse} are not in the result of the translation.
     \item Binary relationships between two tables are directly modeled with a single predicate (not considered here).
 \end{items}

\noindent \textbf{Relational schema} is translated as follows:
 \begin{items}
  \item The RDF representation of a table is of type \texttt{owl:Class} (see triple 4.16 in Figure~\ref{fig:RDF2Course}).
  \item The columns of a table are represented as OWL properties. Columns that represent foreign keys are object properties and the others are datatype properties (see triples 4.17, 4.19 and 4.21 in Figure~\ref{fig:RDF2Course}).
  \item The predicates are typed, i.e.\ we specify domain and range of each object property and domain of each datatype property (see triples 4.18, 4.20, 4.22 and 4.23 in Figure~\ref{fig:RDF2Course}).
 \end{items}

  \begin{figure}[t]
 \small
 \begin{align}
& \textcolor{darkgreen}{\left(\cfo{course},\texttt{rdf:type},\texttt{owl:Class}\right)} \\
& \textcolor{darkgreen}{\left(\texttt{course\#lecture},\texttt{rdf:type},\texttt{owl:DatatypeProperty}\right)} \\
& \textcolor{darkgreen}{\left(\texttt{course\#lecture},\texttt{rdfs:domain},\cfo{course}\right)} \\
& \textcolor{darkgreen}{\left(\texttt{course\#type},\texttt{rdf:type},\texttt{owl:DatatypeProperty}\right)} \\
& \textcolor{darkgreen}{\left(\texttt{course\#type},\texttt{rdfs:domain},\cfo{course}\right)} \\
& \textcolor{darkgreen}{\left(\texttt{course\#room},\texttt{rdf:type},\texttt{owl:ObjectProperty}\right)} \\
& \textcolor{darkgreen}{\left(\texttt{course\#room},\texttt{rdfs:domain},\cfo{course}\right)} \\
& \textcolor{darkgreen}{\left(\texttt{course\#room},\texttt{rdfs:range},\cfo{rooms}\right)} \\
& \left(\texttt{course/lecture=AlgebraI;type=VO},\texttt{rdf:type},\cfo{course}\right)  \\
& \left(\texttt{course/lecture=AlgebraI;type=VO},\texttt{course\#lecture},\mbox{``Algebra I''}\right)  \\
& \left(\texttt{course/lecture=AlgebraI;type=VO},\texttt{course\#type},\mbox{``VO''}\right)  \\
& \textcolor{darkgreen}{\left(\texttt{course/lecture=AlgebraI;type=VO},\texttt{course\#room},\texttt{rooms/room=HS1}\right)} \\
& \left(\texttt{course/lecture=AlgebraI;type=UE},\texttt{rdf:type},\cfo{course}\right)  \\
& \left(\texttt{course/lecture=AlgebraI;type=UE},\texttt{course\#lecture},\mbox{``Algebra I''}\right)  \\
& \left(\texttt{course/lecture=AlgebraI;type=UE},\texttt{course\#type},\mbox{``UE''}\right)  \\
& \textcolor{darkgreen}{\left(\texttt{course/lecture=AlgebraI;type=UE},\texttt{course\#room},\texttt{rooms/room=SEM}\right)}  \\
& \left(\texttt{course/lecture=EconomicsI;type=UE},\texttt{rdf:type},\cfo{course}\right)  \\
& \left(\texttt{course/lecture=EconomicsI;type=UE},\texttt{course\#lecture},\mbox{``Economics I''}\right)  \\
& \left(\texttt{course/lecture=EconomicsI;type=UE},\texttt{course\#type},\mbox{``UE''}\right)  \\
& \textcolor{darkgreen}{\left(\texttt{course/lecture=EconomicsI;type=UE},\texttt{course\#room},\texttt{rooms/room=SEM1}\right)}
 \end{align}
 \caption{The RDF triples obtained by the direct mapping $\mcD\mcM$ \cite{2012Sequeda} from the relational table in Figure~\ref{fig:relCourse3NF}. In \textcolor{darkgreen}{green} are the triples that are in the result of the direct mapping $\mcD\mcM$ but not in the RDB-direct-mapping.}
 \label{fig:RDF2Course}
 \end{figure}
 
\noindent The direct mapping $\mcD\mcM$ is information preserving, query preserving and monotone, but it is not semantics preserving \cite{2012Sequeda}. Consider an instance consisting of two rows with the same primary key, but in the other columns the rows have different values. Such an instance is clearly inconsistent. The result of the direct mapping $\mcD\mcM$ of such an instance is a consistent RDF graph. We have not yet mapped the restrictions enforced by primary and foreign keys. The problem is that OWL does not have a method to specify primary keys. One solution is to encode the violation of a primary key constraint into the mapping. This is done as follows. A datalog rule is defined, which detects a primary key constraint violation. Then, the tuple \texttt{a owl:differentFrom a} is added to the set of RDF triples. This tuple makes the RDF graph inconsistent. This new direct mapping is called $\mcD\mcM_{pk}$. For this direct mapping the following proposition holds.

\begin{proposition}{(Proposition 2 from \cite{2012Sequeda})}
 The direct mapping $\mcD\mcM_{pk}$ is information preserving, query preserving, monotone, and semantics preserving if one considers only primary keys. That is, for every relational schema $R$, set $\Sigma$ of (only) primary keys over $R$ and instance $\ifo{I}$ of $R$: $\ifo{I} \models \Sigma$ iff $\mcD\mcM_{pk}\left(R,\Sigma,\ifo{I}\right)$ is consistent under OWL semantics.
\end{proposition}

\noindent The direct mapping $\mcD\mcM_{pk}$ can be extended with the same idea also to consider foreign keys. Unfortunately, this extension leads to a non-monotone direct mapping. This is because a foreign key inconsistency can be repaired by adding new tuples. But then, the introduced triple \texttt{a owl:differentFrom a} has to be removed from the RDF graph. Hence, the previous model is not a submodel of the new model, thus violating monotonicity.
\end{subsection}

\begin{subsection}{A Direct Mapping of Relational Data to $\DLA$ Knowledge Bases}
\label{ssec:dl_map_rdm}
The direct mapping introduced in the previous section lays the foundations of the mapping we will introduce in this section. This direct mapping translates relational schemas and instances to $\DLA$ KBs. We do not consider primary and foreign keys as data dependencies, we rather focus on functional dependencies. We will show that our mapping is semantics preserving with respect to functional dependencies. First, we will  define a mapping from a relational schema to a $\DLA$ KB, and will later extend this definition with a mapping from functional dependencies to dependencies for $\DLA$. We will call the combination of both mappings \textit{relational to Description Logic direct mapping} (R2DM). \\

\noindent In the following, let $R\left[A_1,\ldots,A_n\right]$ be a relational schema. For the mapping we will use concepts $\cfo{R}$, $\cfo{R\_A_i}$ and roles $\rfo{R\# A_i}$. Tuples occurring in database instances of $R$ are represented by instances of $\cfo{R}$ concepts, a value in a column is represented by an instance of an $\cfo{R\_A_i}$ concept, and the value is then specified by the $\mathit{value}$ value-domain. Without loss of generality, we assume that each column is of the domain \texttt{xsd:string}. The following definition uses dependencies for KBs in form of identification constraints (IdCs) to be defined in the later Section~\ref{sec:dl_fd}. The semantics of the particular IdC is given directly in the definition.

\begin{definition}{(Schema to DL direct mapping ($\sm{}$))} \label{def:dl_sm}
Let $R[U]$ be a relational schema with attributes $U = A_1, \ldots, A_n$. The function $\sm{R[U]}$ outputs a $\DLA$ T-Box $\TRU$ with an IdC $\sigma_{R[U]}$ as follows:

\begin{itemize}
  \item The first set of assertions ensures that the all concepts are disjoint from each other, e.g. an attribute cannot also denote a tuple:
  \begin{align*}
   R &\sqsubseteq \neg R\_A_i & & \forall 1\leq i \leq n \\
   R\_A_i &\sqsubseteq \neg R\_A_j & & \forall 1 \leq i < j \leq n
\end{align*}
   \item Next, we add assertions that express domain and range of a role, mandatory participation to a role as well as domain of an attribute:
\begin{align*}
   \exists R\# A_i &\sqsubseteq R & \exists R\# A_i^- &\sqsubseteq R\_A_i & \forall 0<i\leq n \\
   R &\sqsubseteq \exists R\# A_i & R\_A_i &\sqsubseteq  \exists R\# A_i^- & \forall 0<i\leq n \\
   R\_A_i & \sqsubseteq \delta\left( \mathit{value} \right) & & &  \forall 0<i\leq n \\
   R &\sqsubseteq \neg \delta\left(\mathit{value}\right) & \rho\left( \mathit{value} \right) & \sqsubseteq \texttt{xsd:string} & 
\end{align*}
   \item Last, we add functionality assertions to express that each tuple can only have one of each attribute:
\begin{align*}
    (\mbox{funct } R\# A_i) & & \forall 0 < i \leq n \\
   \left(\mbox{funct } \mathit{value} \right)   
\end{align*}
   \item Additionally, since in the relational model set semantics is assumed, i.e.\ no tuple can occur twice, we add an identification constraint:
   \begin{align*}
   \sigma_{R\left[U\right]} = \id{R}{R\# A_1,\ldots,R\# A_n}.
   \end{align*}
   \noindent This IdC says, that for any two instances of the $R$ concept, if they agree on the instances connected by the $R\#A_1, \ldots, R\#A_n$ roles, then these two instances must be the same.
 \end{itemize}
 
 \noindent The function $\sm{R[U]}$ outputs $\left< \TRU, \sigma_{R\left[U\right]} \right>$.
\end{definition}

\begin{example}
\label{ex:sm_transl}
We will now translate the relational schema $course(lecture,type,room)$ given in Example~\ref{ex:BCNF} to a $\DLA$ KB using the schema-direct mapping, i.e.\ \linebreak $\sm{course(lecture,type,room)}$ outputs the following $\DLA$ TBox:
  \begin{itemize}
  \item Concept disjointness assertions:
  \begin{align*}
   course &\sqsubseteq \neg course\_{lecture} & course &\sqsubseteq \neg course\_{type} \\
   course &\sqsubseteq \neg course\_{room} & course\_{lecture} &\sqsubseteq \neg course\_{type} \\
   course\_{lecture} &\sqsubseteq \neg course\_{room} & course\_{type} &\sqsubseteq \neg course\_{room} 
\end{align*}
   \item Role and attribute property assertions:
\begin{align*}
   \exists course\# lecture &\sqsubseteq course & \exists course\# lecture^- &\sqsubseteq course\_lecture \\
   \exists course\# type &\sqsubseteq course & \exists course\# type^- &\sqsubseteq course\_type \\
   \exists course\# room &\sqsubseteq course & \exists course\# room^- &\sqsubseteq course\_room \\
   course &\sqsubseteq \exists course\# lecture & course\_lecture &\sqsubseteq  \exists course\# lecture^- \\
   course &\sqsubseteq \exists course\# type & course\_type &\sqsubseteq  \exists course\# type^- \\
   course &\sqsubseteq \exists course\# room & course\_room &\sqsubseteq  \exists course\# room^- \\
   course\_lecture & \sqsubseteq \delta\left( \mathit{value} \right) \\
   course\_type & \sqsubseteq \delta\left( \mathit{value} \right) \\
   course\_room & \sqsubseteq \delta\left( \mathit{value} \right) \\
   course & \sqsubseteq \neg \delta\left( \mathit{value} \right) & \rho\left( \mathit{value} \right) & \sqsubseteq \texttt{xsd:string} 
\end{align*}
   \item Functionality assertions:
\begin{align*}
    & (\mbox{funct } course\# lecture) \\
    & (\mbox{funct } course\# type) \\
    & (\mbox{funct } course\# room) \\
   & \left(\mbox{funct } \mathit{value} \right)   
\end{align*}
   \item Identification constraint:
   \begin{align*}
   \id{course}{course\# lecture,course\# type, course\# room} & \qedhere
\end{align*}
 \end{itemize}

\end{example}

\noindent The function $\sm{}$ maps relational schemas to $\DLA$ T-Boxes. Given such a mapping we can translate each model of the KB into an instance of the relational schema and vice versa. We now define such translations. Ideas for the translation and the upcoming proof were taken from \cite{2005berardi}. The function $\im{R[U]}{\ifo{I}}$ translates an instance $\ifo{I}$ of a relational schema $R[U]$ into a model of the KB created by the function $\sm{}$.

\begin{definition}{(Instance to model mapping ($\im{}{}$))} Let $\ifo{I} = (\textbf{dom}^\ifo{I}, T^\ifo{I})$ be an instance of $R[U]$. Let $\left<\TRU,\sigma_{R\left[U\right]} \right>$ denote the result of the function $\sm{R[U]}$. Then, we build the interpretation $\mfo{J} = (\Delta^\mfo{J}, \cdot^\mfo{J})$ of $\left<\TRU,\sigma_{R\left[U\right]}\right>$ as follows:
   
   \begin{itemize}
      \item $\Delta^\mfo{J} = \textbf{dom}^\ifo{I} \cup \{ c_{v,A_i} \mid A_i \in U \wedge v \in T^\ifo{I}\left[A_i\right] \}  \cup \{ t_{\left<d_1,\ldots,d_n\right>} \mid \left< d_1,\ldots,d_n \right> \in T^\ifo{I} \}$, where $c_{v,A_i}$ and $t_{\left<d_1,\ldots,d_n\right>}$ are new elements not yet in $\textbf{dom}^\ifo{I}$
      \item $R^\mfo{J} = \{ t_{\left<d_1,\ldots,d_n\right>} \mid \left<d_1,\ldots,d_n\right> \in T^\ifo{I} \}$,
      \item $R\_ A_i^\mfo{J} = \{ c_{v,A_i} \mid v \in T^\ifo{I}\left[A_i\right] \}$ for all attributes $A_i$ in the relation $R$,
      \item $\mathit{value}^\mfo{J} = \{ (c_{v,A_i},v) \mid v \in T^\ifo{I}\left[A_i\right] \}$ for all attributes $A_i$ in the relation $R$,
      \item $R\# A_i^\mfo{J} = \{ (t_{\left<d_1,\ldots,d_n\right>}, c_{v,A_i}) \mid \left<d_1,\ldots,d_n\right> \in T^\ifo{I} \wedge v = \left<d_1,\ldots,d_n\right>[A_i] \}$ for all attributes $A_i$ in the relation $R$.
   \end{itemize}
   
\noindent The function $\im{R[U]}{\ifo{I}}$ returns $\mfo{J}$.
\end{definition}

\noindent Notice, that for each tuple we create new domain elements $t_{\left<d_1,\ldots,d_n\right>}$, which uniquely identify each tuple in the returned model $\mfo{J}$. We will call such domain elements $t_{\left<d_1,\ldots,d_n\right>}$ \textit{tuple identifiers}. For each value appearing in a column we create new domain elements  $c_{v,A_i}$, which we will call \textit{value identifiers}. 

\begin{example}
\label{ex:im_transl}
We use the instance of Figure~\ref{fig:relCourse3NF} and the relational schema of Example~\ref{ex:BCNF}. We translate the relational schema into a TBox $\TRU$ with the IdC $\sigma_{R\left[U\right]}$ according to the function $\sm{}$ (see Example~\ref{ex:sm_transl}). Now we will map the instance given in Figure~\ref{fig:relCourse3NF} into an interpretation of $\left<\TRU,\sigma_{R\left[U\right]} \right>$. This interpretation is depicted in Figure~\ref{fig:im_transl}. We depict in \textcolor{red}{red} the tuple identifiers and in \textcolor{blue}{blue} the value identifiers. Values are drawn in \textcolor{violet}{violet}.
\begin{figure}[t]
\begin{center}
\input{figures/dl/ex_im_transl.tikz} 
\end{center}
\caption{An interpretation translated by the function $\ffo{i2m}$ from the instance given in Figure~\ref{fig:relCourse3NF}.} 
\label{fig:im_transl}
\end{figure}
\end{example}

\noindent Lemma~\ref{lem:i2m_sound} shows that the model returned by $\im{R[U]}{\mcI}$ is indeed a valid model of $\TRU$ and the IdC $\sigma_{R\left[U\right]}$.

\begin{lemma}
\label{lem:i2m_sound}
Let $R[U]$ be a relational schema, $\left<\TRU,\sigma_{R\left[U\right]}\right>$ be the result of $\sm{R[U]}$, and $\ifo{I}$ be an instance of $R[U]$. Let $\mfo{J}$ be the interpretation returned by $\im{R[U]}{\ifo{I}}$. Then $\mfo{J}$ is a model of $\left<\TRU,\sigma_{R\left[U\right]}\right>$, i.e.\ $\mcJ \models \TRU$ and $\mcJ \models \sigma_{R\left[U\right]}$.
\end{lemma}

\begin{proof}
In order to show that $\mfo{J}$ is a model of $\TRU$ and $\sigma_{R\left[U\right]}$ we need to show that $\mcJ$ satisfies all assertions in $\TRU$ and the IdC $\sigma_{R\left[U\right]}$. 

\begin{itemize}
      \item By the definition of $\sm{R[U]}$ the following assertions appear in $\TRU$:
      \begin{itemize}
      \item $R \sqsubseteq \neg R\_ A_i$: Since $R^\mcJ$ contains only the domain elements not in $\textbf{dom}$, this assertion is satisfied.
      \item $R\_A_i \sqsubseteq \neg R\_ A_j$: For all $i \in \left[1\ldots n\right]$, $R\_A_i ^\mcJ$ contains new domain elements not in any other $R\_A_j ^\mcJ$.
      \item $\exists R\# A_i \sqsubseteq R$, $R \sqsubseteq \exists R\# A_i$: All tuples are in the interpretation of both concepts.
      \item $\exists R\# A_i^- \sqsubseteq R\_A_i$,  $R\_A_i \sqsubseteq  \exists R\# A_i^-$: All attributes are in the interpretation of both concepts.
      \item $(\mbox{funct } R\# A_i)$: For each tuple we construct a single role interpretation.
      \item $(\mbox{funct } \mathit{value})$: A column of a relational tuple cannot be occupied by two values. 
      \end{itemize}
      \item $\sigma_{R\left[U\right]}$ contains the following IdC:
      \begin{itemize}
       \item $\id{R}{R\# A_1,\ldots,R\# A_n}$: Since each tuple is unique, also the identification assertion is satisfied by $\mcJ$.
   \end{itemize}
\end{itemize}
   
\noindent Hence, all assertions in $\left<\TRU,\Sigma\right>$ are satisfied, i.e.\ $\mcJ$ is a valid model of $\TRU$.
\end{proof}

\noindent The function $\mi{\TRU}{\mfo{I}}$ translates a model $\mfo{I}$ of a KB created by $\sm{R[U]}$ into an instance of the relational schema $R[U]$.

\begin{definition}{(Model to instance mapping ($\mi{}{}$))}
$\mfo{I} = (\Delta^\mfo{I}, \cdot^\mfo{I})$ is a model of $\sm{R\left[ U \right]} = \left< \TRU, \sigma_{R\left[U\right]} \right>$. Then we can build a pair $\ifo{J} = \left(\textbf{dom}^\ifo{J}, T^\ifo{J}\right)$ of $R[U]$ as follows:
   
   \begin{itemize}
      \item $\textbf{dom}^\ifo{J} = \Delta^\mfo{I} \setminus \left( R^\mfo{I} \cup \bigcup_{i=1}^n R_{A_i}^\mfo{I}\right)$,
      \item $T^\ifo{J} = \{ \left< v_0, \ldots, v_n \right> \mid \exists t \in R^\mfo{I} \mbox{ s.t. } \bigwedge^n_{i=0} (t,t_i) \in R\# A_i^\mfo{I} \wedge \bigwedge^n_{i=0} (t_i,v_i) \in \mathit{value}^\mfo{I} \}$.
   \end{itemize}
   
\noindent The function $\mi{\TRU}{\mfo{I}}$ returns $\ifo{J}$.
\end{definition}

\noindent Lemma~\ref{lem:m2i_sound} shows that the pair $\ifo{J} = \left(\textbf{dom}^\ifo{J}, T^\ifo{J}\right)$ returned by $\mi{\TRU}{\mfo{J}}$ is indeed an instance of $R[U]$.

\begin{lemma}
\label{lem:m2i_sound}
Let $R[U]$ be a relational schema, $\left<\TRU, \sigma_{R\left[U\right]} \right>$ be the result of $\sm{R[U]}$, and $\mfo{I}$ be a model of $\TRU$. $\ifo{J} = \left(\textbf{dom}^\ifo{J}, T^\ifo{J}\right)$ is the pair returned by $\mi{\TRU}{\mfo{I}}$. Then $\ifo{J}$ is an instance of $R[U]$, i.e.\ $\ifo{J} \models R[U]$.
\end{lemma}

\begin{proof}
We need to check if $\ifo{J}$ is an instance of $R[U]$. Notice that $T^\ifo{J}$ are the tuples of the relation $R$. Because of $\id{R}{R\# A_1, \ldots, R\# A_n}$ a tuple cannot be represented twice in $\mfo{I}$, and therefore each tuple in $T^\ifo{J}$ is unique. Because of the mandatory role participation assertions ($\exists R\# A_i^- \sqsubseteq R\_A_i$) we have at least one value for every attribute of each tuple. Since all roles $R\# A_i$ are functional, we have at most one value for every attribute of each tuple. Hence, each tuple of $T^\ifo{J}$ is a tuple of $R[U]$. Therefore, $\ifo{J}$ is an instance of $R[U]$.
\end{proof}


\noindent So far we have seen that $\im{}{}$ and $\mi{}{}$ generate instances and models. The next lemma will show that the translation of instances to models and back to instances does not lose any information.

\begin{lemma}
\label{lem:drm_instance}
Let $R[U]$ be a relational schema and let $\left<\TRU,\sigma_{R\left[U\right]}\right>$ be the result of $\sm{R[U]}$. Let $\ifo{I}$ be an instance of $R[U]$, then $\ifo{I} = \mi{\TRU}{\im{R[U]}{\ifo{I}}}$.
\end{lemma}

\begin{proof}
By Lemma~\ref{lem:i2m_sound} $\im{R[U]}{\ifo{I}}$ outputs a model $\mfo{J}$ of $\TRU$. Additionally, each tuple of $\ifo{I}$ is identified by a unique tuple identifier $t_{\left<d_1,\ldots,d_n\right>}$ and no other tuple identifiers are generated. Each tuple identifier has $n$ associated value identifiers, each connected to a single value. Since by Lemma~\ref{lem:m2i_sound}, $\mi{\TRU}{\mfo{J}}$ outputs an instance which has exactly the same tuples as $\ifo{I}$. Therefore, $I = \mi{\TRU}{\im{R[U]}{\ifo{I}}}$.
\end{proof}

\noindent It is also possible to translate models to instances and back to models. But, we will then loose some information. During the translation from models to instances we drop the domain elements which represent tuple and value identifiers. Then, when we translate the instance back to a model, we generate new domain elements for tuple and value identifiers. Those are not necessarily the same as before. But, it is possible to map to each tuple and value identifier from the original model an identifier of the new model. Thus, we can show in the next lemma that the two models are isomorphic.

\pagebreak
\begin{lemma}
\label{lem:drm_model}
Let $R[U]$ be a relational schema and let $\left<\TRU,\sigma_{R\left[U\right]}\right>$ be the result of $\sm{R[U]}$. Let $\mfo{I}$ be a model of $\TRU$, then $\mfo{I} \cong \im{\TRU}{\mi{R[U]}{\mfo{I}}}$.
\end{lemma}

\begin{proof}
By Lemma~\ref{lem:m2i_sound} $\mi{R[U]}{\mfo{I}}$ outputs an instance $\ifo{J}$ of $R[U]$. The function $\im{\TRU}{\ifo{J}}$ then outputs a model $\mfo{I}^\prime$. In order to show that $\mfo{I} \cong \im{\TRU}{\mi{R[U]}{\mfo{I}}}$, we are going to construct an isomorphism between $\mfo{I}$ and $\mfo{I}^\prime$, therefore we define a bijective function $h: \Delta^\mfo{I} \ra \Delta^{\mfo{I}^\prime}$. Since, $\mi{}{}$ and $\im{}{}$ only change the tuple and value identifiers we map all other domain element to themselves:

\begin{itemize}
 \item for all $d \in \Delta^\mfo{I} \setminus \{ R^\mfo{I} \cup \bigcup_{i=1}^n R_{A_i}^\mfo{I}\}$: $h\left(d\right) = d$
\end{itemize}

\noindent It remains to map the tuple and value identifiers, which are the domain elements in $R^\mfo{I}$ and $R\_A_i^\mfo{I}$. Since $\mfo{I}$ is a valid model of $\TRU$, each $t \in R^\mfo{I}$ is connected by an $R\# A_i$ role to an $R\_A_i$ concept $c_i$. These $c_i$ objects are connected to values $d_i$, which are used in $\im{}{}$ to generate the tuple identifier $t_{\left<d_1,\ldots,d_n\right>}$. Therefore, we map each $t \in R^\mfo{I}$ to the corresponding tuple identifier $t_{\left<d_1,\ldots,d_n\right>}$, and each $c_i \in R\_A_i^\mfo{I}$ to the corresponding value identifier.

\begin{itemize}
 \item for all $A_i \in U$ and for all $c_i \in R\_A_i^\mfo{I}$: $h\left(c_i\right) = {c_{v,A_i}}^{\mfo{I}^\prime}$, such that $\left(c_i,v\right) \in \mathit{value}^\mfo{I}$,
 \item for all $t \in R^\mfo{I}$: $h\left(t\right) = {t_{\left<d_1,\ldots,d_n\right>}}^{\mfo{I}^\prime}$, such that for all $d_i$ it holds that 
 $\left(t,c_i\right)^\mfo{I} \in R\# A_i$ and  $\left(c_i,d_i\right) \in \mathit{value}^\mfo{I}$.
\end{itemize}


\noindent Since each $t$ object in $R^\mfo{I}$ is connected to the same $d_i$ object as the tuple identifiers in $\mfo{I}^\prime$, it holds that for all roles $R \in \ffo{roles}(\mcT)$ and for all $\left(a,b\right) \in \Delta^\mfo{I} \times \Delta^\mfo{I}: \left(a,b\right) \in R^\mfo{I}$ if and only if \linebreak $\left(h\left(a\right),\left(b\right)\right) \in R^{\mfo{I}^\prime}$. Additionally, since every $t \in R^\mfo{I}$ has a corresponding tuple identifier ${t_{\left<d_1,\ldots,d_n\right>}}^{\mfo{I}^\prime} \in R^{\mfo{I}^\prime}$ and all other domain elements are mapped to the same elements, also for all concepts $C \in \ffo{concepts}(\mcT)$ and for all $a \in \Delta^\mfo{I}: a \in C^\mfo{I} \mbox{ if and only if } h\left(a\right) \in C^{\mfo{I}^\prime}$ holds. Therefore, $\mfo{I} \cong \im{\TRU}{\mi{R[U]}{\mfo{I}}}$.
\end{proof}

\begin{example}
\label{ex:m2i_iso}
We use the relational schema $course$ of Example~\ref{ex:BCNF}. Let $\mcT_{course}$ be the KB given in Example~\ref{ex:sm_transl}. The model $\mcM$ in Figure~\ref{fig:im_iso} is a valid model of the KB $\mcT_{course}$. The function $\mi{\mcT_{course}}{\mcM}$ returns the instance given in Figure~\ref{fig:relCourse3NF}. The application of the function $\im{}{}$ to that instance returns the model given in Figure~\ref{fig:im_transl} (see Example~\ref{ex:im_transl}). Let us denote this model with $\mcM^\prime$. We will now show that these two models are isomorphic. We map the domain elements of $\mcM$ and $\mcM^\prime$ as follows:
\begin{itemize}
 \item First, we map all domain elements not in $course^{\mcM}$, $course\_lecture^{\mcM}$, $course\_type^{\mcM}$ and $course\_room^{\mcM}$ to themselves:
 \begin{align*}
  h(\mathtt{Algebra I}^\mcM) &= \mathtt{Algebra I}^{\mcM^\prime} & h(\mathtt{Economics}^\mcM) &= \mathtt{Economics}^{\mcM^\prime} \\
  h(\mathtt{VO}^\mcM) &= \mathtt{VO}^{\mcM^\prime} & h(\mathtt{UE}^\mcM) &= \mathtt{UE}^{\mcM^\prime} \\
  h(\mathtt{HS1}^\mcM) &= \mathtt{HS1}^{\mcM^\prime} & h(\mathtt{SEM1}^\mcM) &= \mathtt{SEM1}^{\mcM^\prime}
 \end{align*}
 \item Then, we map all tuple identifiers:
 \begin{align*}
  h\left(t_1^\mcM\right) &= t_{\left<\textit{Algebra I, VO, HS1}\right>}^{\mcM^\prime} \\
  h\left(t_2^\mcM\right) &= t_{\left<\textit{Algebra I, UE, SEM1}\right>}^{\mcM^\prime} \\
  h\left(t_3^\mcM\right) &= t_{\left<\textit{Economics I, UE, SEM1}\right>}^{\mcM^\prime},
 \end{align*}
 \item and the value identifiers in $course\_lecture^{\mcM}$, $course\_type^{\mcM}$ and $course\_room^{\mcM}$:
 \begin{align*}
  h\left(cl_1^\mcM\right) &= c_{\textit{lecture,Algebra I}}^{\mcM^\prime} & 
  h\left(ct_1^\mcM\right) &= c_{\textit{type,VO}}^{\mcM^\prime} & 
  h\left(cr_1^\mcM\right) &= c_{\textit{room,HS1}}^{\mcM^\prime} \\
  h\left(cl_2^\mcM\right) &= c_{\textit{lecture,Economics I}}^{\mcM^\prime} & 
  h\left(ct_2^\mcM\right) &= c_{\textit{type,UE}}^{\mcM^\prime} & 
  h\left(cr_2^\mcM\right) &= c_{\textit{room,SEM1}}^{\mcM^\prime} \\
 \end{align*}
\end{itemize}

\noindent It is easy to verify that $h\left(\cdot\right)$ is indeed an isomorphism.
\end{example}

\begin{figure}[t]
\begin{center}
\input{figures/dl/ex_im_iso.tikz} 
\end{center}
\caption{The model $\mcM_{course}$.} 
\label{fig:im_iso}
\end{figure}

\noindent We can now associate the set of instances to the set of valid models of a KB created by the function $\sm{}$. As a result the next corollary directly follows from Lemma~\ref{lem:drm_instance} and~\ref{lem:drm_model}.

\pagebreak
\begin{corollary}
\label{cor:mappingSemantics}
Let $R[U]$ be a relational schema and let $\left<\TRU,\sigma_{R\left[U\right]}\right>$ be the result of \linebreak $\sm{R[U]}$. Then $$\ffo{Inst}\left(R[U]\right) = \{ \mi{\TRU}{\mfo{I}} \mid \mfo{I} \models \TRU \wedge \mfo{I} \models \sigma_{R\left[U\right]} \}$$ and $$\ffo{Mod}\left(\left< \TRU, \sigma_{R\left[U\right]} \right> \right) = \ffo{Closure}_{\cong} \left( \{ \im{R[U]}{\ifo{I}} \mid \ifo{I} \in \ffo{Inst}\left(R[U]\right) \} \right).$$
\end{corollary}
\end{subsection}
\end{section}

\begin{section}{Data Dependencies}
\label{sec:dl_fd}

In this section we will investigate data dependencies in DLs. DLs already include different types of data dependencies. For example, concept inclusions are a form of data dependencies. Even though functionality assertions exist for DLs, it is so far not possible to model FD-like constraints over DL KBs. Functional dependencies express identification properties. In particular, in conceptual modeling it is often needed to specify that an object is uniquely identified by some of its properties. For example, a person is identified by its social security number. Thus, it is important to extend DLs with such dependencies. \\

\noindent Calvanese et al.\ introduce path-based identification constraints (pIdCs) as a mechanism for functional dependencies in $\DLA$ \cite{2008calvanese}. We will introduce pIdCs in Section~\ref{ssec:dl_fd_pidc}. We will investigate if we can find a direct mapping of FDs to pIdCs, such that the direct-mapping is semantics preserving. Unfortunately, in Section~\ref{ssec:dl_fd_sem} we show that we cannot extend the direct-mapping with pIdCs such that it is semantics preserving. Therefore, we will introduce in Section~\ref{ssec:dl_fd_tidc} an extension to pIdCs, called tree-based identification constraints (tIdCs), which allows us to give a semantics preserving relational to Description Logic direct-mapping.

\begin{subsection}{Path-based identification constraints}
\label{ssec:dl_fd_pidc}
\noindent Path-based identification constraints (pIdCs) were introduced by Calvanese et al.\ \cite{2008calvanese} for various DLs. We focus on pIdCs for $\DLA$ KBs. A (path-based) identification constraint states that a concept can be identified by some particular properties. These properties are paths. A path $\pi$ over a $\DLA$ KB is given by the following expression:
    $$\pi \ra S \mid D? \mid \pi \circ \pi,$$
    
\noindent where $S$ denotes a basic role or attribute, $D$ denotes a basic concept or value-domain and $\pi \circ \pi$ denotes the composition of paths. $D?$ is a test relation, which represents the identity relation on instances of $D$. Test relations can be used to formulate paths over instances of a specific class. For example, the path $\rfo{HAS\mhyphen CHILD} \circ \cfo{Woman}?$ connects someone with his/her daughters. \\

\noindent A path can be seen as a complex property for an object $o$. An object that is reachable by $\pi$ from $o$ is called a \textit{$\pi$-filler} for $o$. An object $o$ can have several or no $\pi$-fillers. The length of a path $\pi$, denoted by $\ffo{length}\left(\pi\right)$ is inductively defined:
\begin{align*}
 \ffo{length}\left(\pi\right) &= \begin{cases}
                                    0 & \mbox{if } \pi = D?, \\
                                    1 & \mbox{if } \pi = S, \\
                                    \ffo{length}\left(\pi_1\right) + \ffo{length}\left(\pi_2\right) & \mbox{if } \pi = \pi_1 \circ \pi_2.
                                 \end{cases}
\end{align*}

\noindent We are now able to give a definition for path-based identification constraints.
    
    \begin{definition}{(pIdC \cite{2008calvanese, 2009calvanese})}
     A \textit{path-based identification constraint} (pIdC) over a $\DLA$ KB is an assertion of the form
     $$\id{C}{\pi_1\ldots\pi_n}$$
     where $C$ denotes a basic concept, $n\geq1$, and $\pi_1\ldots\pi_n$ (called the \textit{components} of the identifier) are paths over $\DLA$ such that $length(\pi_i) \geq 1$ for all $i \in \left[1\ldots n\right]$.
    \end{definition}
    
\noindent Such a pIdC intuitively states, that if there two objects $o$ and $o^\prime$, such that they share a $\pi_i$-fillers for every $i \in [1\ldots n]$, then these two objects must be the same. For example, we can say that no two men can have the same daughters with the pIdC $\id{\cfo{Man}}{\rfo{HAS\text{-}CHILD \circ \cfo{Woman}?}}$. We will call a pIdC \textit{local}, if at least one path $\pi_i$ has the length of one. We can now define $\DLA$ with pIdCs:

\begin{definition}{($\DLAId$ KB with pIdCs \cite{2008calvanese})}
   A KB in $\DLAId$, that is $\DLA$ with pIdCs, is a pair $\left<\mcT,\mcA\right>$, where $\mcA$ is a $\DLA$ ABox, and $\mcT$ is the union of two sets $\mcT_\mcA$ and $\mcT_{id}$, where $\mcT_\mcA$ is a $\DLA$ TBox, and $\mcT_{id}$ is a set of pIdCs such that
   
   \begin{items}
    \item all concepts in a pIdC of $\mcT_{id}$ are basic concepts;
    \item for each pIdC $\alpha$ in $\mcT_{id}$, every role or attribute that occurs (in either direct or inverse direction) in a path of $\alpha$ does not appear in the right-hand side of assertions of the form $Q \sqsubseteq Q^\prime$ or $U \sqsubseteq U^\prime$. \qedhere
   \end{items}
\end{definition}

\noindent Notice that the last constraint is a generalization of the constraint already imposed over functionality assertions in $\DLA$ KBs.  \\

\noindent We now need to define the semantics of pIdCs. First, we define the semantics of a path $\pi$, which is given by an extension $\pi^\mcI$ in an interpretation $\mcI$ as follows:

\begin{items}
     \item if $\pi = S$, then $\pi^\mcI = S^\mcI$,
     \item if $\pi = D?$, then $\pi^\mcI = \left\{ \left(o,o\right) | o \in D^\mcI \right\}$,
     \item if $\pi = \pi_1 \circ \pi_2$, then $\pi^\mcI = \pi^\mcI_1 \circ \pi^\mcI_2$, where $\circ$ denotes the composition operator on relations.
\end{items}
    
\noindent We denote with $\pi^\mcI\left(o\right)$ the set of $\pi$-fillers for $o$ in $\mcI$. A $\pi$-filler is every object that is reachable from $o$ in $\mcI$ by means of $\pi$, i.e.\ $\pi^\mcI\left(o\right) = \left\{o^\prime \mid \left(o,o^\prime\right) \in \pi^\mcI \right\}$. Then, an interpretation $\mcI$ satisfies the IdC $\id{C}{\pi_1\ldots\pi_n}$ if for all $o,o^\prime \in C^\mcI$, $\pi^\mcI_1\left(o\right) \cap \pi^\mcI_1\left(o^\prime\right) \neq \emptyset \wedge \cdots \wedge \pi^\mcI_n\left(o\right) \cap \pi^\mcI_n\left(o^\prime\right) \neq \emptyset$ implies $o = o^\prime$. 

\begin{subsubsection}{KB satisfiability with pIdCs}
\label{sssec:pidcs_sat}

  We will investigate $\DLA$ KB satisfiability with pIdCs in the presence of weakly-acyclic KBs. It has been shown that $\DLAId$ KB satisfiability with arbitrary pIdCs is \NLOGSPACE-hard with respect to the ABox (see Theorem 6 of \cite{2008calvanese}), whereas KB satisfiability with local pIdCs is \LOGSPACE-complete with respect to the ABox. The second is proven by a perfect reformulation of a query that asks for the violation of some pIdC in a $\DLAId$ KB. If such a query returns false, i.e.\ no pIdC is violated, then the $\DLAId$ KB is satisfiable. We will show that we can also evaluate such a query over the canonical model of a satisfiable weakly-acyclic $\DLA$ KB. \\
  
  \noindent First, we will define a translation of a pIdC $\alpha$ to a CQ with an inequality $\delta\left(\alpha\right)$ that encodes the violation of $\alpha$. We will use the following translation function where $B$ is a basic concept and $x$ is a variable \cite{2009calvanese}:
  
  \begin{gather*}
    \gamma\left(B,x\right) = \begin{cases}
                              A\left(x\right), & \mbox{if } B=A, \\
                              P\left(x,y_{new}\right), & \mbox{if } B=\exists P, \mbox{ where } y_{new} \mbox{ is a fresh variable}, \\
                              P\left(y_{new},x\right), & \mbox{if } B=\exists P^-, \mbox{ where } y_{new} \mbox{ is a fresh variable}.
                             \end{cases}
  \end{gather*}
  \noindent Let the IdC $\alpha$ be of the form $\id{B}{\pi_1,\ldots,\pi_n}$. Then, we define a CQ with an inequality
  \begin{gather*}
   \delta\left(\alpha\right)\left(x,x^\prime\right) = \exists\mathbf{x}.\gamma\left(B,x\right) \wedge \gamma\left(B,x^\prime\right) \wedge x \neq x^\prime \wedge \bigwedge_{1\leq i \leq n} \left( \rho\left(\pi_i,x,x_i\right) \wedge \rho\left(\pi_i,x^\prime,x_i\right)\right),
  \end{gather*}
  where $\mathbf{x}$ are all variables appearing in the atoms of $\delta\left(\alpha\right)$ except for $x$ and $x^\prime$. The translation function $\rho\left(\pi,x,y\right)$ is inductively defined on the structure of the path $\pi$ as follows:
  \begin{items}
   \item[(1)] If $\pi = B_1? \circ \cdots B_h? \circ Q \circ B^\prime_1? \circ \cdots \circ B^\prime_k?$ (with $h \geq 0, k\geq 0$), then
   \begin{gather*}
    \rho\left(\pi,x,y\right) = \gamma\left(B_1,x\right) \wedge \cdots \wedge \gamma\left(B_h,x\right) \wedge Q\left(x,y\right) \wedge \gamma\left(B^\prime_1,y\right) \wedge \cdots \wedge \gamma\left(B^\prime_k,y\right).
   \end{gather*}
   \item[(2)] If $\pi = \pi_1 \circ \pi_2$, where $\ffo{length}\left(\pi_1\right) = 1$ and $\ffo{length}\left(\pi_2\right) \geq 1$, then
   \begin{gather*}
    \rho\left(\pi,x,y\right) = \rho\left(\pi_1,x,z\right) \wedge \rho\left(\pi_2,z,y\right),
   \end{gather*}
   \noindent where $z$ is a fresh variable symbol not occurring elsewhere in the query.
  \end{items}
  
  \noindent Intuitively, the query $\delta\left(\alpha\right)\left(x,x^\prime\right)$ asks for two different individuals $x, x^\prime$, such that for all $i \in [1\ldots n]$ the path $\pi_i$ starting from $x$ and $x^\prime$ end at the same individual $x_i$. If the query returns such individuals then these two witness a violation of $\alpha$.  Now consider a $\DLAId$ KB $\mcK = \left< \mcT \cup \mcT_{id}, \mcA \right>$, where $\mcT$ is a $\DLA$ TBox and $\mcT_{id}$ is a set of pIdCs. Then, the boolean UCQ
  \begin{gather*}
   q_{\mcT_{id}} = \bigcup_{\alpha \in \mcT_{id}} \exists x_\alpha, x_\alpha^\prime \left\{ \delta\left(\alpha\right)\left(x_\alpha,x^\prime_\alpha\right) \right\},
  \end{gather*}
  \noindent asks for a violation of some pIdC in $\mcT_{id}$. If the query $q_{\mcT_{id}}$ is true then there is one query $\delta\left(\alpha\right)\left(x_\alpha,x_\alpha^\prime\right)$ that returns two individuals $x_\alpha$ and $x_\alpha^\prime$, that witness the violation of some pIdC $\alpha$. We can now show the following:
  
  \begin{theorem}
  \label{thm:pIdCs_sat}
    Let $\mcK = \left< \mcT, \mcA \right>$ be a satisfiable weakly-acyclic $\DLA$ KB, let $\mcT_{id}$ be a set of pIdCs, and let $q_{\mcT_{id}}$ be a UCQ as defined above. Then the $\DLAId$ KB $\mcK_{id} = \left< \mcT \cup \mcT_{id}, \mcA \right>$ is satisfiable if and only if $q_{\mcT_{id}}^{\ffo{can}\left(\mcK\right)} = \emptyset$.
  \end{theorem}

  \begin{proof} $\;$
  \begin{itemize}
    \item[($\Ra$)] Suppose $\mcK_{id}$ is satisfiable. We need to show that then $q_{\mcT_{id}}^{\ffo{can}\left(\mcK\right)} = \emptyset$. Assume towards a contradiction that $q_{\mcT_{id}}^{\ffo{can}\left(\mcK\right)}$ returns true. But then, there exists a pIdC $\alpha$ such that there are two constants $x$, $x^\prime$ that witness the violation of $\alpha$ in $\ffo{can}\left(\mcK\right)$. Therefore, $\mcK_{id}$ is unsatisfiable, which contradicts our assumption.
    \item[($\La$)] Suppose $q_{\mcT_{id}}^{\ffo{can}\left(\mcK\right)} = \emptyset$. We need to show that then $\mcK_{id}$ is satisfiable. Since no pIdC violates $\ffo{can}\left(\mcK\right)$, $\ffo{can}\left(\mcK\right)$ is also a model of $\mcK_{id}$. \qedhere
   \end{itemize}
  \end{proof}
\end{subsubsection}

\begin{subsubsection}{Implication of pIdCs}
\label{sssec:pidcs_impl}
 We will now look at the implication problem for pIdCs. That is, given a weakly-acyclic $\DLA$ TBox $\mcT$, a set of pIdCs $\mcT_{id}$ and a pIdC $\alpha$, check whether $\left\{ \mcT \cup \mcT_{id} \right\} \models \alpha$, i.e.\ every model of $\mcT$ and $\mcT_{id}$ also satisfies $\alpha$. \\
 
 \noindent Additionally, we define the notion of \emph{trivially} implied pIdCs. An FD $X \ra Y$ is trivially implied if $Y \subseteq X$. Intuitively, this means that $X \ra Y$ is trivially holds if $X$ uniquely determines a subset of attributes of itself. We can generalize this notion for pIdCs. Consider the pIdC $\varphi = \id{C}{\pi}$ where $\pi$ is an arbitrary path. Then, the pIdC $\id{C}{\pi \circ \pi^- \circ C?}$ is \emph{trivially} implied by $\varphi$. This can be generalized to the following, if both $\id{C}{\pi}$ and $\id{B}{\pi_1 \circ C? \circ \pi}$, where $\pi$ and $\pi_1$ are arbitrary paths, are in the set of implied pIdCs, then the pIdC $\id{B}{\pi_1 \circ C? \circ \pi \circ \pi^- \circ C?}$ is \emph{trivially} implied. Trivial implication in pIdCs follows from the fact, that if a concept $C$ is uniquely determined by a path $\pi$, we can walk back the path $\pi$ to the concept $C$. We will end at the same individual. Hence, at the concept we started from. Since, $C$ trivially implies itself, the above holds. \\
 
 \noindent We can decide implication of pIdCs by, first, creating a $\DLAId$ ABox $\mcA_\alpha$ that violates the pIdC $\alpha$. Then, we chase the $\DLA$ KB $\mcK = \left< \mcT, \mcA_\alpha \right>$, i.e.\ we add all membership assertions implied by $\mcT$. Finally, we use the pIdCs in $\mcT_{id}$ and the functionality assertions in $\mcT$, denoted by $\mcT_f$, to merge constants in $\ffo{chase}\left(\mcK\right)$, in order to verify the violation of $\alpha$. This is implemented by the algorithm \textsf{IdCImpl}, illustrated in Algorithm~\ref{alg:pIdC_impl}.\\
 
 \begin{algorithm}[t]
   \SetKwInOut{Input}{input}
\SetKwInOut{Output}{output}

\Input{$\DLA$ TBox $\mcT$, a set of pIdCs $\mcT_{id}$, a pIdC $\alpha$}
\Output{true if $\mcT \cup \mcT_{id} \models \alpha$}

\BlankLine

 $\mcT_f^{id} \ra \emptyset$\;
 create the counter-model ABox $\mcA_\alpha$ from $\alpha$\;
 $\mcA \la \ffo{chase}\left(\left< \mcT, \mcA_\alpha \right>\right)$\;
 \ForEach{functionality assertion $\funct{Q}$}{
    $\mcT_f^{id} \la \mcT_f^{id} \cup \left\{ \id{\top}{Q^-} \right\}$\;
 }
 \Repeat{$\mcA^\prime = \mcA$}{
    $\mcA^\prime \la \mcA$\;
    \ForEach{pIdC $\beta \in \mcT_{id} \cup  \mcT_f^{id}$}{
       \If{$\left(x,x^\prime\right) \in \delta\left(\beta\right)^\mcA$}{
          \eIf{$x = x_0 \wedge x^\prime = y_0$}{
             \Return{true}\;
          }{
             $\mcA \la \mcA[x/z][x^\prime/z]$, where $z$ is a fresh object not yet in $\mcA$\;
          }
       }
    }
 }
 \Return{false}
 \BlankLine
 \caption{The algorithm \textsf{IdCImpl} for deciding the implication of pIdCs}
 \label{alg:pIdC_impl} 
 \end{algorithm}
 
 \pagebreak
 
 \noindent For the illustration of Algorithm~\ref{alg:pIdC_impl} we will use the following running example.
 
 \begin{example}
 \label{ex:pIdC_Impl1}
  Let us consider the $\DLA$ TBox $\mcT$ over the concept $A$, and the roles $P, F, S$. The TBox $\mcT$ contains the concept inclusion
  $$A \sqsubseteq \exists P.$$
  \noindent Let the set of pIdCs $\mcT_{id}$ be the following:
  \begin{align*}
   \id{\exists P^-}{P^- \circ F \circ P}, & & \id{\exists P^-}{P^- \circ S \circ P}.
  \end{align*}
  \noindent We want to check if the above implies the pIdC
  \begin{gather*}
    \alpha = \id{A}{P^- \circ A? \circ F \circ A? \circ S \circ A?},
  \end{gather*}
  
  \noindent i.e. $\mcT \cup \mcT_{id} \models \alpha$.
 \end{example}
 
 \pagebreak
 
 \noindent As a first step in Algorithm~\ref{alg:pIdC_impl} we define an ABox $\mcA_\alpha$, which we will call counter-model ABox. Given a pIdC $\alpha = \id{B}{\pi_1, \ldots, \pi_n}$, such an ABox $\mcA_\alpha$ consists of the following set of membership assertions:

  \begin{align*}
      A_\alpha = \left\{ \gamma(B,x_0), \gamma(B,y_0) \right\} \cup \bigcup_{1 \leq i \leq n} \left\{ \varrho\left(\pi_i\left(x_0,z_i\right)\right) \cup \varrho\left(\pi_i\left(y_0,z_i\right)\right) \right\},
  \end{align*}
  
  \noindent where $\gamma(B,x)$ is the translation function as defined in Section~\ref{sssec:pidcs_sat} and the translation function $\varrho$ is defined on the structure of the path $\pi$ as follows:

  \begin{items}
      \item[(1)] If $\pi = B_1? \circ \cdots B_h? \circ Q \circ B^\prime_1? \circ \cdots \circ B^\prime_k?$ (with $h \geq 0, k\geq 0$), then
   \begin{gather*}
    \varrho\left(\pi\left(x,y\right)\right) = \gamma\left(B_1,x\right) \cup \cdots \cup \gamma\left(B_h,x\right) \cup Q\left(x,y\right) \cup \gamma\left(B^\prime_1,y\right) \cup \cdots \cup \gamma\left(B^\prime_k,y\right).
   \end{gather*}
   \item[(2)] If $\pi = \pi_1 \circ \pi_2$, where $\ffo{length}\left(\pi_1\right) = 1$ and $\ffo{length}\left(\pi_2\right) \geq 1$, then
   \begin{gather*}
    \varrho\left(\pi\left(x,y\right)\right) = \varrho\left(\pi_1\left(x,z\right)\right) \cup \varrho\left(\pi_2\left(z,y\right)\right),
   \end{gather*}
   \noindent where $z$ is a fresh variable symbol not occurring elsewhere in the ABox.
  \end{items}
  
  \noindent Next, we use the chase to materialize the missing membership assertions, i.e.\ $\ffo{chase}\left(\mcK\right)$ of the KB $\mcK = \left< \mcT, \mcA_\alpha \right>$. 
  
  \begin{example}
  \label{ex:pIdC_Impl2}
   This example continues Example~\ref{ex:pIdC_Impl1}. The ABox $\mcA_\alpha$ built from the pIdC $\alpha$ is depicted in Figure~\ref{fig:ex_pIdC_Impl1}. Then we chase the KB $\mcK = \left< \mcT, \mcA_\alpha \right>$, which adds the membership assertions as shown in Figure~\ref{fig:ex_pIdC_Impl2}.
  \end{example}

  \begin{figure}[t]
  \begin{center}
  \input{figures/dl/ex_pIdC_Imp1.tikz} 
   \end{center}
   \caption{The counter-model ABox $\mcA_\alpha$.}  
   \label{fig:ex_pIdC_Impl1}
   \end{figure}
   
   \begin{figure}[t]
  \begin{center}
  \input{figures/dl/ex_pIdC_Imp2.tikz} 
   \end{center}
   \caption{The chase of the KB $\mcK = \left<\mcT,\mcA_\alpha\right>$ adds the membership assertions drawn in \textcolor{red}{red}.}  
   \label{fig:ex_pIdC_Impl2}
   \end{figure}
   
   \noindent We will now chase the membership assertions in $\ffo{chase}\left(\mcK\right)$ with the pIdCs in $\mcT_{id}$ and the functionality assertions in $\mcT$ as follows:
   
   \begin{items}
    \item[(1)] First, we create a pIdC for each functionality assertion in $\mcT_f$ as follows:
    \begin{align*}
     \mbox{if } \funct{Q} \in \mcT_f & \mbox{ then } \id{\top}{Q^-}.
    \end{align*}
    \noindent We will denote by $\mcT_f^{id}$ this newly created set of pIdCs.
    \item[(2)] Then, we translate each pIdC $\beta$ in $\mcT_{id} \cup \mcT_f^{id}$ to the CQ $\delta(\beta)$, which asks for a violation of $\beta$. 
    \item[(3)] If the query $\delta(\beta)$ evaluated over $\DB{\ffo{chase}\left(\mcA_\alpha\right)}$ returns a tuple of objects $(x,y)$ that witnesses a violation of a pIdC, we substitute the objects $x$ and $y$ in $\ffo{chase}\left(\mcA_\alpha\right)$ with a new object $z$ not yet in $\mcA_\alpha$.
    \item[(4)] We repeat (3) until 
    \begin{items}
     \item[(a)] either the objects $x_0$ and $y_0$ are returned by a CQ  $\delta(\beta)$, which means that the pIdC $\alpha$ is implied by $\mcT \cup \mcT_{id}$ or
     \item[(b)] no further CQ returns a tuple, which means that $\alpha$ is not implied by $\mcT \cup \mcT_{id}$.
    \end{items}
   \end{items}
   
   \begin{example}
     We continue Example~\ref{ex:pIdC_Impl2}. We have translated each pIdC in $\mcT_{id} \cup \mcT_f^{id}$ to a CQ. The CQ of the pIdC $\id{\exists P^-}{P^- \circ S \circ P}$ evaluated over the ABox in Figure~\ref{fig:ex_pIdC_Impl2} returns the tuples $\left\{ (x_2^\prime, y_2^\prime), (y_2^\prime, x_2^\prime) \right\}$. Therefore, the objects $x_2^\prime$ and $y_2^\prime$ are removed and substituted with a new object $z_2^\prime$. The resulting ABox is illustrated in Figure~\ref{fig:ex_pIdC_Impl3}. This new ABox violates the pIdC $\id{\exists P^-}{P^- \circ F \circ P}$. The corresponding CQ returns the tuples $\left\{ (x_0^\prime, y_0^\prime), (y_0^\prime, x_0^\prime) \right\}$. Therefore, the algorithm \textsf{IdCImpl} returns true. Hence, $\mcT \cup \mcT_{id} \models \alpha$.
   \end{example}

   \begin{figure}[t]
  \begin{center}
  \input{figures/dl/ex_pIdC_Imp3.tikz} 
   \end{center}
   \caption{The ABox after we have applied the pIdC $\id{\exists P^-}{P^- \circ S \circ P}$.}  
   \label{fig:ex_pIdC_Impl3}
   \end{figure}
   
   \noindent We will now show the correctness of Algorithm~\ref{alg:pIdC_impl}.
   
   \begin{theorem}
   \label{thm:pidcs_impl}
    Let $\mcT$ be a weakly-acyclic satisfiable $\DLA$ TBox, let $\mcT_{id}$ be a set of pIdCs and let $\alpha$ be a pIdC. Then, \textsf{IdCImpl} returns true if and only if $\mcT \cup \mcT_{id} \models \alpha$. 
   \end{theorem}
   
   \begin{proof}[Proof idea.]
    Notice that the algorithm $\textsf{IdCImpl}$ mimics the chase with weakly-acyclic tuple-generating dependencies (tgds) and equality-generating dependencies (egds) \cite{1995databases,2005fagin}, i.e.\ we can view the counter-model ABox as a database, positive inclusion dependencies in the TBox as tgds and identification constraints as egds. Then, $\textsf{IdCImpl}$ and the chase coincides, therefore soundness and completeness of the algorithm $\textsf{IdCImpl}$ can be proved similarly as soundness and completeness of the chase with weakly-acyclic tgds and egds \cite{1995databases,2005fagin}.
   \end{proof}
\end{subsubsection}

\begin{subsubsection}{Path-based IdCs as a formalism to model functional dependencies in $\DLA$}
 We will show how to model unary functional dependencies with path-based identification constraints in $\DLA$. Let $R[A,B]$ be a relational schema, and let $A \ra B$ be an FD over $R[A,B]$. We can map the relational schema to a $\DLA$ KB using the schema to DL direct mapping introduced in Definition~\ref{def:dl_sm}. We can extend this $\DLA$ KB with pIdCs to express the FD $A\ra B$, which is translated to the pIdC:
 
 $$\id{R\_B}{R\#B^- \circ R\#A}.$$
 
 \noindent Let us now consider two different instances of the relational schema $R[A,B]$. Instance $\ifo{I}_1$ given in Figure~\ref{fig:ex_pIdC_I1} satisfies the FD $A \ra B$, where the instance $\ifo{I}_2$ in Figure~\ref{fig:ex_pIdC_I2} does not satisfy this FD. If we now look at the translated models given in Figures~\ref{fig:ex_pIdC_M1} and~\ref{fig:ex_pIdC_M2}, we observe the same. That is, the model $\mcM_1$ satisfies the translated pIdC and the model $\mcM_2$ does not. Unfortunately, a natural generalization for such a translation to $n$-ary FDs fails. This will be investigated in the upcoming section.
 
 \begin{figure}[t]
\begin{center}
 \begin{subfigure}[b]{0.45\textwidth}
 \centering
 \begin{minipage}[c]{0.45\textwidth}
 \begin{tabular}{r|c|c}
  & A & B \\
  \hline $t_1$ & $a_1$ & $b_1$
 \end{tabular}
  \end{minipage}
 \caption{Instance $\ifo{I}_1$: $\ifo{I}_1 \models A \ra B$}
 \label{fig:ex_pIdC_I1}
 \end{subfigure}
 \begin{subfigure}[b]{0.45\textwidth}
 \centering
 \begin{minipage}[c]{0.45\textwidth}
 \begin{tabular}{r|c|c}
  & A & B  \\
  \hline $t^\prime_1$ & $a^\prime_1$ & $b^\prime_1$  \\
  $t^\prime_2$ & $a^\prime_1$ & $b^\prime_2$ 
 \end{tabular}
 \end{minipage}
  \caption{Instance $\ifo{I}_2$: $\ifo{I}_2 \nmodels A \ra B$}
  \label{fig:ex_pIdC_I2}
\end{subfigure}
 \begin{subfigure}[c]{0.45\textwidth}
  \centering\input{figures/dl/ex-pidc_i1.tikz}
  \caption{Model $\mfo{M}_1 = \ffo{i2m}_{R\left[U\right]}\left(\ifo{I}_1\right)$: \newline $\mfo{M}_1 \models \id{R\_B}{R\#B^- \circ R\#A}$}
  \label{fig:ex_pIdC_M1}
\end{subfigure}
\begin{subfigure}[c]{0.45\textwidth}
  \centering\input{figures/dl/ex-pidc_i2.tikz}
  \caption{Model $\mfo{M}_2 = \ffo{i2m}_{R\left[U\right]}\left(\ifo{I}_2\right)$: \newline $\mfo{M}_2 \nmodels \id{R\_B}{R\#B^- \circ R\#A}$}
  \label{fig:ex_pIdC_M2}
\end{subfigure}
\end{center}
\caption{Instances and their mapping into $\DLA$ interpretations.}
\label{fig:ex_pIdC}
\end{figure}


\end{subsubsection}
\end{subsection}

\begin{subsection}{FDs and pIdCs are semantically different}
\label{ssec:dl_fd_sem}

We have seen how to model unary FDs in $\DLA$ KBs with pIdCs. However, this can not be generalized to non-unary FDs. We will show that two instances of a relational schema can be distinguished by FDs, i.e.\ one instance satisfies the FD and the other does not, but the translated pIdCs can not distinguish the translated models. The next example illustrates such a case.

\begin{example}
\label{ex:FD_IdC}
Consider the FD $\sigma := AB \ra C$ and the pIdC \\ $\delta := \id{R\_C}{R\# C^- \circ R\# A, R\# C^- \circ R\# B}$ translated from $\sigma$. We will now show that $\sigma$ and $\delta$ distinguish different relational instances and $\DLA$ models. In Figure~\ref{fig:FD_IdC} we give two instances of a relational schema $R\left[A,B,C\right]$. The instance $\ifo{I}_1$ is a valid instance satisfying the FD $\sigma$, whereas the instance $\ifo{I}_2$ is not a valid instance for the FD $\sigma$. If we now translate $\sigma$ into a pIdC $\delta$ and also use $\im{}{}$ to map the instances $\ifo{I}_1$ and $\ifo{I}_2$ to the models $\mfo{M}_1$ and $\mfo{M}_2$ respectively, we get two models that both violate the translated pIdC $\delta$ (see Figure~\ref{fig:FD_IdC_M1} and~\ref{fig:FD_IdC_M2}). Notice that the model $\mfo{M}_1$, without the objects and roles given in red, viewed as an ABox, is the counter-model ABox for the implication of the pIdC $\delta$.\end{example}

\begin{figure}[t]
\begin{center}
 \begin{subfigure}[b]{0.45\textwidth}
 \centering
 \begin{minipage}[c]{0.45\textwidth}
 \begin{tabular}{r|c|c|c}
  & A & B & C \\
  \hline $t^\prime_1$ & $a^\prime_1$ & $b^\prime_2$ & $c^\prime_1$ \\
  $t^\prime_2$ & $a^\prime_2$ & $b^\prime_1$ & $c^\prime_1$ \\
  $t^\prime_3$ & $a^\prime_3$ & $b^\prime_1$ & $c^\prime_2$ \\
  $t^\prime_4$ & $a^\prime_1$ & $b^\prime_3$ & $c^\prime_2$ 
 \end{tabular}
  \end{minipage}
 \caption{Instance $\ifo{I}_1$: $\ifo{I}_1 \models \sigma$}
 \label{fig:FD_IdC_I1}
 \end{subfigure}
 \begin{subfigure}[b]{0.45\textwidth}
 \centering
 \begin{minipage}[c]{0.45\textwidth}
 \begin{tabular}{r|c|c|c}
  & A & B & C \\
  \hline $t_1$ & $a_1$ & $b_1$ & $c_1$ \\
  $t_2$ & $a_1$ & $b_1$ & $c_2$
 \end{tabular}
 \end{minipage}
  \caption{Instance $\ifo{I}_2$: $\ifo{I}_2 \nmodels \sigma$}
  \label{fig:FD_IdC_I2}
\end{subfigure}
 \begin{subfigure}[b]{0.45\textwidth}
  \centering\input{figures/dl/FD_pIdC_i1.tikz}
  \caption{Model $\mfo{M}_1 = \ffo{i2m}_{R\left[U\right]}\left(\ifo{I}_1\right)$: $\mfo{M}_1 \nmodels \delta$}
  \label{fig:FD_IdC_M1}
\end{subfigure}
\begin{subfigure}[b]{0.45\textwidth}
  \centering\input{figures/dl/FD_pIdC_i2.tikz}
  \caption{Model $\mfo{M}_2 = \ffo{i2m}_{R\left[U\right]}\left(\ifo{I}_2\right)$: $\mfo{M}_2 \nmodels \delta$}
  \label{fig:FD_IdC_M2}
\end{subfigure}
\end{center}
\caption{Instances and their mapping into RDF graphs. The FD $AB \ra C$ can distinguish the two structures $\ifo{I}_1$ and $\ifo{I}_2$, whereas the pIdC $\id{R\_C}{R\# C^- \circ R\# A, R\# C^- \circ R\# B}$ cannot distinguish the two models $\mfo{M}_1$ and $\mfo{M}_2$.}
\label{fig:FD_IdC}
\end{figure}

\noindent Example~\ref{ex:FD_IdC} just shows that $\delta$ is not a correct translation of the FD $\sigma$, s.t. $\mfo{M}_1 \models \delta$ and $\mfo{M}_2 \nmodels \delta$. In order to show that pIdCs are indeed not able to capture the differences in $\mfo{M}_1$ and $\mfo{M}_2$, we need to prove that for any set of IdCs $\Sigma$ it holds that whenever $\mfo{M}_1 \models \Sigma$, then $\mfo{M}_2 \models \Sigma$. Such a proof is established in Theorem~\ref{thm:FdIdCmismatch}.

\begin{theorem}
\label{thm:FdIdCmismatch}
There is a set $\FD$ of functional dependencies over a relational schema $R[U]$, and a pair of relational instances $I_1$ and $I_2$ of $R[U]$, s.t. for any set $\Sigma$ of pIdCs the following holds:
\begin{itemize}
 \item[(a)] $I_1 \models \FD$ and $I_2 \nmodels \FD$, and
 \item[(b)] $\im{R[U]}{I_1} \nmodels \Sigma$ or $\im{R[U]}{I_2} \models \Sigma$.
\end{itemize}
\end{theorem}

\noindent Before we proof Theorem~\ref{thm:FdIdCmismatch} we need some preliminary notions. Let us first consider the following claim, which establishes the relationship between objects that are in bisimulation and their $\pi$-fillers.

\begin{claim}
\label{clm:bisim_path}
Let $\pi$ be an arbitrary path in $\DLA$, let $o_1 \in \Delta^\mfo{I}$ and $o_2 \in \Delta^\mfo{J}$. If $o_1 \sim_\mcB o_2$ then $\pi^\mfo{I}\left(o_1\right) \sim_\mcB \pi^\mfo{J}\left(o_2\right)$.
\end{claim}

\noindent The proof of Claim~\ref{clm:bisim_path} directly follows from Definition~\ref{def:bisim} (Bisimulations). In order to prove Theorem~\ref{thm:FdIdCmismatch}, we need to have established a bisimulation between the two models in Example~\ref{ex:FD_IdC}.

\begin{claim}
 \label{clm:bisim_instances}
 The models $\mfo{M}_1$ and $\mfo{M}_2$ of Example~\ref{ex:FD_IdC} are in bisimulation to each other, i.e.\ $\mfo{M}_1 \sim_\mcB \mfo{M}_2$.
\end{claim}

\begin{proof}
 Table~\ref{tab:biSim} shows the domain elements that bisimulate each other in the corresponding structures. It is easily verified that the relation in Table~\ref{tab:biSim} is indeed a bisimulation of $\mfo{M}_1$ and $\mfo{M}_2$. \qedhere
\begin{table}[htbp]
 \begin{center}
  \setlength{\tabcolsep}{3pt}
  \begin{tabular}{c|c|c|c|c|c|c|c|c|c|c|c|c}
   \backslashbox{$\mfo{M}_2$}{$\mfo{M}_1$} & $t^\prime_1$ & $t^\prime_2$ & $t^\prime_3$ & $t^\prime_4$ & $a^\prime_1$ & $a^\prime_2$ & $a^\prime_3$ & $b^\prime_1$ & $b^\prime_2$ & $b^\prime_3$ & $c^\prime_1$ & $c^\prime_2$ \\
   \hline $t_1$ & $\sim_\mcB$ & $\sim_\mcB$ & $\sim_\mcB$ & $\sim_\mcB$ & & & & & & & & \\
   \hline $t_2$ & $\sim_\mcB$ & $\sim_\mcB$ & $\sim_\mcB$ & $\sim_\mcB$ & & & & & & & & \\
   \hline $a_1$ & & & & & $\sim_\mcB$ & $\sim_\mcB$ & $\sim_\mcB$ & & & & & \\
   \hline $b_1$ & & & & & & & & $\sim_\mcB$ & $\sim_\mcB$ & $\sim_\mcB$ & & \\
   \hline $c_1$ & & & & & & & & & & & $\sim_\mcB$ & $\sim_\mcB$ \\
   \hline $c_2$ & & & & & & & & & & & $\sim_\mcB$ & $\sim_\mcB$ 
  \end{tabular}
 \end{center}
 \caption{Bisimulation relation of $\mfo{M}_1 \sim_\mcB \mfo{M}_2$}
 \label{tab:biSim}
\end{table}
\end{proof}

\noindent With a proof for the bisimulation of $\mfo{M}_1$ and $\mfo{M}_2$ we are ready to prove Theorem~\ref{thm:FdIdCmismatch}.

\begin{proof}{(of Theorem~\ref{thm:FdIdCmismatch})}
Let $AB \ra C$ be the only functional dependency in the set $\FD$. Suppose $\Sigma$ is an arbitrary set of pIdCs. Let $\ifo{I}_1$ and $\ifo{I}_2$ be the two instances of Example~\ref{ex:FD_IdC}. We now show based on the pIdCs contained in $\Sigma$ that (a) and (b) hold.

\begin{itemize}
 \item Suppose $\Sigma = \emptyset$: 
 \begin{itemize}
  \item[(a)] As illustrated in Example~\ref{ex:FD_IdC}, $I_1 \models \FD$ and $I_2 \nmodels \FD$.
  \item[(b)] Clearly, $\im{R[U]}{I_2} \models \Sigma$ holds.
 \end{itemize}
 \item Suppose there is an arbitrary pIdC $\sigma_C \in \Sigma$, which is of the form $\id{R\_C}{\pi_1,\ldots,\pi_n}$ in $\Sigma$:
 \begin{itemize}
 \item[(a)] As illustrated in Example~\ref{ex:FD_IdC}, $I_1 \models \FD$ and $I_2 \nmodels \FD$.
 \item[(b)] Let $\mfo{M}_1$ denote $\im{R[U]}{\ifo{I}_1}$ and let $\mfo{M}_2$ denote $\im{R[U]}{\ifo{I}_2}$. Observe that by Claim~\ref{clm:bisim_instances} $\mfo{M}_1 \sim_\mcB \mfo{M}_2$. Suppose $\im{R[U]}{\ifo{I}_2} \nmodels \sigma_C$, i.e.\ $\mfo{M}_2 \nmodels \sigma_C$. We need to show that then $\im{R[U]}{\ifo{I}_1} \nmodels \sigma_C$, i.e.\ $\mfo{M}_1 \nmodels\sigma_C$. Since $\mfo{M}_2 \nmodels \sigma_C$ there are two $C$-objects ($c^\prime_1$ \& $c^\prime_2$), s.t.\ ${\pi_1}^{\mfo{M}_2}(c^\prime_1) \cap {\pi_1}^{\mfo{M}_2}(c^\prime_2) \neq \emptyset \wedge \ldots \wedge {\pi_n}^{\mfo{M}_2}(c^\prime_1) \cap {\pi_n}^{\mfo{M}_2}(c^\prime_2) \neq \emptyset$. Since $c^\prime_1 \sim_\mcB c_1$ and $c^\prime_2 \sim_\mcB c_2$, we will show that $c^\prime_1$ and $c^\prime_2$ also violate $\sigma_C$.
 
 In addition to Claim~\ref{clm:bisim_instances}, we observe the following property in $\mcM_1$ and $\mcM_2$. For any object $o$ in $\mcM_2$ and any path $\pi$, if $o^\prime \sim_\mcB o$ and $o \in \pi^{\mcM_2}\left(c_1\right)$ and $o \in \pi^{\mcM_2}\left(c_2\right)$, then $o^\prime \in \pi^{\mcM_2}\left(c_1^\prime\right)$ and $o^\prime \in \pi^{\mcM_2}\left(c_2^\prime\right)$.
 
 Let us now denote, for an arbitrary $j \in \left[1\ldots n\right]$, with $x \in \Delta^{\mfo{M}_2}$ an arbitrary object in ${\pi_j}^{\mfo{M}_2}(c^\prime_1) \cap {\pi_j}^{\mfo{M}_2}(c^\prime_2)$. Since for every object $o \in \Delta^{\mfo{M}_2}$, there is also an object $o^\prime \in \Delta^{\mfo{M}_1}$, such that $o \sim_\mcB o^\prime$, there is also an object $y \in \Delta^{\mfo{M}_1}$ such that $x \sim_B y$. Since $x \in \pi^{\mcM_2}\left(c_1\right)$ and $x \in \pi^{\mcM_2}\left(c_2\right)$ and the previous observation, we can conclude that $y \in \pi^{\mcM_2}\left(c_1\right)$ and $y \in \pi^{\mcM_2}\left(c_2\right)$. Therefore, $y \in {\pi_j}^{\mfo{M}_1}(c_1^\prime) \cap {\pi_j}^{\mfo{M}_1}(c_2^\prime)$. Hence,  ${\pi_j}^{\mfo{M}_1}(c_1^\prime) \cap {\pi_j}^{\mfo{M}_1}(c_2^\prime) \neq \emptyset$ for all $j \in \left[1\ldots n\right]$, which proves that $\mfo{M}_1 \nmodels \sigma_C$.
\end{itemize}

 \item Suppose there is an arbitrary IdC $\sigma_{AB} \in \Sigma$, which is of the form $\id{X}{\pi^i_1,\ldots,\pi^i_n}$ in $\Sigma$, where $X$ is either $R\_A$ or $R\_B$:
 \begin{itemize}
 \item[(a)] As illustrated in Example~\ref{ex:FD_IdC}, $I_1 \models \sigma$ and $I_2 \nmodels \sigma$.
 \item[(b)] Let $\mfo{M}_2$ denote $\im{R[U]}{\ifo{I}_2}$. $\mfo{M}_2$ has only one instance of an $R\_A$ ($R\_B$) concept, therefore $\mfo{M}_2 \models \sigma_{AB}$ trivially holds.\qedhere\end{itemize}\end{itemize}\end{proof}

\noindent We have now shown in Theorem~\ref{thm:FdIdCmismatch}, that it is possible to have two instances of a relational schema, s.t.\ in one instance an FD is satisfied and in the other the FD is violated. If we now translate these two instances by the schema direct mapping into models of $\DLA$, we cannot find an IdC such that this IdC is satisfied in one model and violated in the other. Thus the following corollary follows from Theorem~\ref{thm:FdIdCmismatch}.

\begin{corollary}
 The schema direct mapping to $\DLA$ KB $\left(\sm{}\right)$ extended with a mapping from FDs to pIdCs is not semantics preserving.
\end{corollary}

\noindent The problem in the translation of the FD $AB \ra C$ in Example~\ref{ex:FD_IdC} comes from the fact that the attributes $A$, $B$ and $C$ only refer to the columns in exactly one row. The pIdC allows one to talk about different rows. Consider the pIdC $\id{R\_C}{R\# C^- \circ R\# A, R\# C^- \circ R\# B}$. The object reachable by $R\# C^-$ in the path $R\# C^- \circ R\# A$ and in the path $R\# C^- \circ R\# B$ might be different, as illustrated in Figure~\ref{fig:FD_IdC_M1}. In order to achieve a semantics preserving mapping we need to ensure that this object is the same in all paths. In the next section we propose a syntactic and semantic extension of pIdC which allows for such expressions. This extension is called tree-based identification constraints.
\end{subsection}


\begin{subsection}{Tree-based identification constraints}
\label{ssec:dl_fd_tidc}
In order to correctly capture the semantics of FDs, we extend path-based identification constraints to tree-based identification constraints. Let $\tau$ denote a \textit{tree} built by the following syntax, where $S$ denotes a role and $D$ denotes a concept, and $\pi$ denotes a path as defined in Section~\ref{ssec:dl_fd_pidc}:
\begin{align*}
 \tau & \ra \pi \mid \pi \circ \left( \tau, \ldots, \tau \right)
\end{align*}
\noindent A tree $\tau$ evaluates over instances of concepts as follows: Let $o$ be an object in an interpretation $\mfo{I}$. The tuple representing the objects at the leaves of a tree $\tau$ starting from $o$ in $\mfo{I}$ , is called a $\tau$-\textit{filler} for $o$. If the tree $\tau$ has just one leaf, i.e.\ it is a path, then the $\tau$-filler coincides with the definition of a $\pi$-filler given in \cite{2008calvanese}. For convenience if $\left( \tau, \ldots, \tau \right)$ has just one path $\pi$ we do not write the brackets, i.e.\ instead of $\pi \circ (\tau)$ we write $\pi \circ \tau$. Analogously to paths, we define the \emph{depth} and the \emph{width} of a tree. The depth is the equivalent to the length of paths, and inductively defined as follows: 

\begin{align*}
 \ffo{depth}\left(\tau\right) &= \begin{cases}
                                    \ffo{length}\left(\pi\right) & \mbox{if } \tau \mbox{ is a path } \pi \\
                                    \ffo{length}\left(\pi\right) + \ffo{max}\left(\ffo{depth}\left(\tau_1\right),\ldots,\ffo{depth}\left(\tau_n\right)\right) & \mbox{if } \tau \mbox{ is a tree } \pi \circ \left(\tau_1,\ldots,\tau_n\right)
                                 \end{cases}
\end{align*}

\noindent The width of a tree is the number of leaves and is inductively defined as follows:

\begin{align*}
 \ffo{width}\left(\tau\right) &= \begin{cases}
                                    1 & \mbox{if } \tau \mbox{ is a path } \pi \\
                                    \sum_{i = 1}^n \ffo{width}\left(\tau_i\right) & \mbox{if } \tau \mbox{ is a tree } \pi \circ \left( \tau_1,\ldots,\tau_n\right)
                                 \end{cases}
\end{align*}

\noindent Tree-based identification constraints (tIdCs) are an extension to pIdCs and are defined as follows.

\begin{definition}{(Tree-based identification constraints (tIdC))}
 A \textit{tree-based identification constraint} over a $\DLA$ KB is an assertion of the form $$\id{C}{\tau_1, \ldots, \tau_n}$$ where $C$ is a basic concept in $\DLA$, $n \geq 1$, and $\tau_1,\ldots,\tau_n$ (called the \emph{components} of the identifier) are trees over a $\DLA$ KB such that $\ffo{depth}\left(\tau_i\right) \geq 1$ for all $i \in \left[1\ldots n\right]$.
\end{definition}

\noindent We adapt the definition of a $\DLAId$ KB to include tree-based identification constraints.

\begin{definition}{($\DLAtid$ KB with tIdCs)}
   A KB in $\DLAtid$, that is $\DLA$ with tIdCs, is a pair $\left<\mcT,\mcA\right>$, where $\mcA$ is a $\DLA$ ABox, and $\mcT$ is the union of the two sets $\mcT_\mcA$ and $\mcT_{tid}$, where $\mcT_\mcA$ is a $\DLA$ TBox, and $\mcT_{tid}$ is a set of tIdCs such that
   
   \begin{items}
    \item all concepts identified in $\mcT_{tid}$ are basic concepts;
    \item all concepts appearing in the test relations in $\mcT_{tid}$ are basic concepts, or basic value-domains;
    \item for each tIdC $\alpha$ in $\mcT_{tid}$, every role or attribute that occurs (in either direct or inverse direction) in a path of $\alpha$ does not appear in the right-hand side of assertions of the form $Q \sqsubseteq Q^\prime$ or $U \sqsubseteq U^\prime$. \qedhere
   \end{items}
\end{definition}

\noindent The semantics of a tree $\tau$ is given by an extension $\tau^\mfo{I}$ in an interpretation $\mfo{I}$ as follows:

\begin{itemize}
 \item if $\tau = \pi$, then $\tau^\mfo{I} = \pi^\mfo{I}$
 \item if $\tau = \pi \circ \left( \tau_1, \ldots, \tau_n \right)$, then 
 \begin{align*}
 \tau^\mfo{I} = \left\{ \left(o,\left< o^1_1, \ldots, o^1_k, \cdots, o^n_1, \ldots, o^n_l \right>\right) \right. \mid & \exists o^\prime.\left(o, o^\prime\right) \in \pi^\mfo{I} \wedge \\ & \left(o^\prime,\left< o^1_1, \ldots, o^1_k \right>\right) \in \tau_1^\mfo{I} \wedge \\
                     & \;\;\;\;\;\;\;\;\; \vdots \\
                     & \left. \left(o^\prime,\left< o^n_1, \ldots, o^n_l \right>\right) \in \tau_n^\mfo{I} \right\},\end{align*}
\end{itemize}

\noindent where $\pi^\mcI$ is the extension already defined by pIdCs. The $\tau$-filler for an object $o$ and a tree $\tau$, denoted by $\tau^\mcI\left(o\right)$, is a set of tuples with arity $\ffo{width}\left(\tau\right)$. Intuitively, the interpretation of a tree $\tau$ maps the root node of the tree with its leaves. \\

\noindent An interpretation $\mfo{I}$ satisfies the tree-based identification constraint $\id{C}{\tau_1, \ldots, \tau_n}$ if for all $o, o^\prime \in C^\mfo{I}$, $\tau_1^\mfo{I}\left(o\right) \cap \tau_1^\mfo{I}\left(o^\prime\right) \neq \emptyset \wedge \ldots \wedge \tau_n^\mfo{I}\left(o\right) \cap \tau_n^\mfo{I}\left(o^\prime\right) \neq \emptyset$ implies $o = o^\prime$. Example~\ref{ex:treeIdC} illustrates tree-based identification constraints.

\begin{example}
\label{ex:treeIdC}
Let us show how to distinguish the two models given in Example~\ref{ex:FD_IdC} with tIdCs. The translation of the FD $AB \ra C$ to tIdCs is as follows:
\begin{align}
 \id{R\_C}{R\#C^- \circ \left(R\#A, R\#B \right)} \label{eqn:treeIdC}
\end{align}
\noindent The evaluation of above IdC over the interpretation given in Figure~\ref{fig:FD_IdC_M1} is given in Table~\ref{tab:tIdC_M1}. We first write the binary tuples that are in the interpretation of the roles $R\#A$, $R\#B$ and $R\#C^-$. We then, after the vertical line, combine these to tuples of objects according to the semantics of tIdCs. \\
\begin{table}[h]
 \begin{center}
 %\setlength{\tabcolsep}{1pt}
 \begin{tabular}{cccccc}
  $R\#C^-$ & $\circ \left( \right.$ & $R\#A$ & , & $R\#B$ & $\left.\right)$ \\ \hline
  $\left(c^\prime_1,t^\prime_1\right)$ & & $\left(t^\prime_1,a^\prime_1\right)$ & & $\left(t^\prime_1,b^\prime_3\right)$ \\
  $\left(c^\prime_1,t^\prime_4\right)$ & & $\left(t^\prime_4,a^\prime_2\right)$ & & $\left(t^\prime_4,b^\prime_1\right)$ \\
  $\left(c^\prime_2,t^\prime_2\right)$ & & $\left(t^\prime_2,a^\prime_1\right)$ & & $\left(t^\prime_2,b^\prime_2\right)$ \\
  $\left(c^\prime_2,t^\prime_3\right)$ & & $\left(t^\prime_3,a^\prime_3\right)$ & & $\left(t^\prime_2,b^\prime_1\right)$ \\ \hline
  \multicolumn{6}{c}{$\left(c^\prime_1,\left<a^\prime_1,b^\prime_3\right>\right)$} \\
  \multicolumn{6}{c}{$\left(c^\prime_1,\left<a^\prime_2,b^\prime_1\right>\right)$} \\
  \multicolumn{6}{c}{$\left(c^\prime_2,\left<a^\prime_1,b^\prime_2\right>\right)$} \\
  \multicolumn{6}{c}{$\left(c^\prime_2,\left<a^\prime_3,b^\prime_1\right>\right)$} \\ \hline
 \end{tabular}
 \end{center}
 \caption{Evaluation of the tIdC given in Equation~\ref{eqn:treeIdC} over the interpretation in Figure
~\ref{fig:FD_IdC_M1}}
 \label{tab:tIdC_M1}
\end{table}

\noindent Notice that the tuples in Table~\ref{tab:tIdC_M1} correspond to the tuples in the relational instance given in Figure~\ref{fig:FD_IdC_I1}. Let us check for the violation of the tIdC given in Equation~\ref{eqn:treeIdC}. The only two different objects of type $R\_C$ are $c^\prime_1$ and $c^\prime_2$. The $\tau$-filler for $c^\prime_1$ is the set $\left(\left<a^\prime_1,b^\prime_3\right>,\left< a^\prime_2,b^\prime_1 \right>\right)$ and the $\tau$-filler for $c^\prime_2$ is the set $\left(\left<a^\prime_1,b^\prime_2\right>,\left< a^\prime_3,b^\prime_1 \right>\right)$. The intersection of the two sets is empty, therefore the tIdC is not violated. It is easy to see that
\begin{gather*}
\mcM_1 \models \id{R\_C}{R\#C^- \circ \left(R\#A, R\#B \right)}. \qedhere
\end{gather*}
\end{example}

\noindent In comparison to pIdCs, tIdCs allows us to specify that several paths must walk through common nodes, and split afterwards. In this sense, every pIdC can be represented a tIdC, but not vice versa. Therefore, tIdCs are more expressive than pIdCs.

\begin{subsubsection}{KB satisfiability with tIdCs}
\label{sssec:tidcs_sat}

  We will investigate $\DLA$ KB satisfiability with tIdCs in the presence of weakly-acyclic KBs. We will extend the method introduced for pIdCs in Section~\ref{sssec:pidcs_sat}. First, we will define a translation of a tIdC $\alpha$ to a CQ with an inequality $\delta^t\left(\alpha\right)$ that encodes the violation of $\alpha$. For paths we will use the translation $\rho$ defined in Section~\ref{sssec:pidcs_sat}.\\
  
  \noindent Let the tIdC $\alpha$ be of the form $\id{B}{\tau_1,\ldots,\tau_n}$. Then, we define a CQ with inequality
  \begin{align*}
   \delta^t\left(\alpha\right)\left(x,x^\prime\right)  = \; & \exists\mathbf{x}.\gamma\left(B,x\right) \wedge \gamma\left(B,x^\prime\right) \wedge x \neq x^\prime \wedge \\ 
   & \bigwedge_{1 \leq i \leq n} \rho^t\left(\tau_i,x,\left< x^i_1, \ldots x^i_{\ffo{width}\left(\tau_i\right)}\right>\right) \wedge \rho^t\left(\tau_i,x^\prime,\left< x^i_1, \ldots, x^i_{\ffo{width}\left(\tau_i\right)} \right>\right),
  \end{align*}
  where $\mathbf{x}$ are all variables appearing in the atoms of $\delta^t\left(\alpha\right)$ except for $x$ and $x^\prime$. The translation function $\rho^t\left(\tau,x,\left< x_1, \ldots, x_k\right>\right)$ is inductively defined on the structure of the tree $\tau$ as follows:
  \begin{items}
   \item[(1)] If $\tau = \pi$, then
   \begin{gather*}
    \rho^t\left(\tau,x,\left< y \right>\right) = \rho\left(\pi,x,y\right)
   \end{gather*}
   \item[(2)] If $\tau = \pi \circ \left(\tau_1, \ldots, \tau_l\right)$, then
   \begin{align*}
    \rho^t\left(\tau,x,\left< x_1, \ldots, x_k\right>\right) = & \rho\left(\pi,x,z\right) \wedge \\ 
    & \rho^t\left(\tau_1,z,\left< x_1, \ldots, x_{\ffo{width}\left(\tau_1\right)}\right>\right) \wedge \\ 
    & \vdots \\ & \rho^t\left(\tau_l,z,\left<x_{1+\sum_{j=1}^{l-1} \ffo{width}\left(\tau_l\right)},\ldots,x_k\right>\right),
   \end{align*}
   
   \noindent where $z$ is a fresh variable symbol not occurring elsewhere in the query.
  \end{items}
  
  \noindent The query has the following intuition. First, we ask for two different individuals $x$ and $x^\prime$. These individuals must be instances of $B$. Additionally, they share for every tree $\tau$ in the tIdC a tuple at the leafs of $\tau$ starting in $x$ and $x^\prime$. If $\delta^t\left(\alpha\right)\left(x,x^\prime\right)$ returns two such individuals then the tIdC $\alpha$ is violated. Now consider a $\DLAtid$ KB $\mcK = \left< \mcT \cup \mcT_{tid}, \mcA \right>$, where $\mcT$ is a $\DLA$ TBox and $\mcT_{tid}$ is a set of tIdCs. Then, the boolean UCQs
  \begin{gather*}
   q_{\mcT_{tid}} = \bigcup_{\alpha \in \mcT_{tid}} \exists x_\alpha,x_\alpha^\prime \left\{ \delta^t\left(\alpha\right)\left(x_\alpha,x^\prime_\alpha\right) \right\},
  \end{gather*}
  \noindent where $\mathbf{x}$ are the variables in the UCQ $q_{\mcT_{tid}}$, asks for a violation of any tIdC in $\mcT_{tid}$. We can now show the following:
  
  \begin{theorem}
    Let $\mcK = \left< \mcT, \mcA \right>$ be a satisfiable weakly-acyclic $\DLA$ KB, let $\mcT_{tid}$ be a set of tIdCs, and let $q_{\mcT_{tid}}$ be a UCQs as defined above. Then the $\DLAtid$ KB $\mcK_{tid} = \left< \mcT \cup \mcT_{tid}, \mcA \right>$ is satisfiable if and only if $q_{\mcT_{tid}}^{\ffo{can}\left(\mcK\right)} = \emptyset$.
  \end{theorem}

  \begin{proof} The proof is similar to the proof of Theorem~\ref{thm:pIdCs_sat} for pIdCs.
  \end{proof}
\end{subsubsection}

\begin{subsubsection}{Implication of tIdCs}
\label{sssec:tidcs_impl}
 The implication problem for tIdCs can be solved using the algorithm \textsf{IdCImpl}, established in Section~\ref{sssec:pidcs_impl}. We just need to adapt the construction of the counter-model ABox for tIdCs. \\

 \noindent Given a weakly-acyclic $\DLA$ TBox $\mcT$, a set of tIdCs $\mcT_{tid}$ and a tIdC \linebreak $\alpha = \id{B}{\tau_1, \ldots, \tau_n}$, we want to check whether $\left\{ \mcT \cup \mcT_{tid} \right\} \models \alpha$. We define a counter-model ABox $\mcA_\alpha$ of $\alpha$ consisting of the following set of membership assertions:

  \begin{align*}
      A_\alpha = & \left\{ \gamma(B,x_0), \gamma(B,y_0) \right\} \cup \\
                 & \bigcup_{1 \leq i \leq n} \left\{ \varrho^t\left(\tau_i\left(x_0,\left< z^i_1, \ldots, z^i_{\ffo{width}\left(\tau_i\right)}\right>\right)\right) \cup \varrho^t\left(\tau_i\left(y_1,\left< z^i_1, \ldots, z^i_{\ffo{width}\left(\tau_i\right)}\right>\right)\right) \right\},
  \end{align*}
  
  \noindent where $\gamma(B,x)$ is the translation function as defined in Section~\ref{sssec:pidcs_sat} and the translation function $\varrho^t$ is defined on the structure of the tree $\tau$ as follows:

  \begin{items}
   \item[(1)] If $\tau = \pi$, then
   \begin{gather*}
    \varrho^t\left(\pi\left(x,\left< y \right>\right)\right) = \varrho\left(\pi\left(x,y\right)\right)
   \end{gather*}
   \item[(2)] If $\tau = \pi \circ \left(\tau_1, \ldots, \tau_l\right)$, then
   \begin{align*}
    \varrho^t\left(\tau\left(x,\left< x_1, \ldots, x_k\right>\right)\right) = & \varrho\left(x,z\right) \cup \\ 
    & \varrho^t\left(\tau_1\left(z,\left< x_1, \ldots, x_{\ffo{width}\left(\tau_1\right)}\right>\right)\right) \cup \\ 
    & \vdots \\ & \varrho^t\left(\tau_l\left(z,\left<x_{1+\sum_{j=1}^{l-1} \ffo{width}\left(\tau_j\right)},\ldots,x_k\right> \right)\right),
   \end{align*}
   
   \noindent where $z$ is a fresh variable symbol not occurring elsewhere in the query.
  \end{items}
   
   \begin{theorem}
    Let $\mcT$ be a weakly-acyclic satisfiable $\DLA$ TBox, let $\mcT_{tid}$ be a set of tIdCs and let $\alpha$ be a tIdC. Then, \textsf{IdCImpl}, adapted to tIdCs, returns true if and only if $\mcT \cup \mcT_{tid} \models \alpha$. 
   \end{theorem}
   
   \begin{proof}
    This proof is similar to the proof of Theorem~\ref{thm:pidcs_impl} for pIdCs.
   \end{proof}
\end{subsubsection}

\begin{subsubsection}{The Direct-Mapping of FDs to IdCs}

\noindent We will now extend the schema direct mapping with a mapping from functional dependencies to tree-based identification constraints. In this section we will then prove that this mapping is semantics preserving. First, let us translate FDs to tIdCs.

 \begin{definition}{(FD-direct mapping ($\dm{}$))}
Let $U$ be a set of attributes $A_1,\ldots,A_n$. Given a relational schema $R\left[U\right]$, and a set of functional dependencies $\FD$ over $R\left[U\right]$, the function $\dm{R\left[U\right],\FD}$ outputs a set of $\DLA$ tree-based identification assertions $\Sigma_\FD$ as follows:

\vspace{5mm}
\noindent Let $X$ be a set of attributes $A_{i_1}, \ldots, A_{i_k}$. For each FD $X \ra A_i \in \FD$ we add a tIdC to $\Sigma_{\FD}$:
 \begin{align*}
   \id{R\_A_i}{R\# A_i^- \circ R? \circ \left( R \# A_{j_1} \circ A_{j_1}?, \ldots, R \# A_{j_k} \circ A_{j_k}? \right)}
\end{align*}

\noindent The function $\dm{R\left[U\right],\FD}$ outputs $\Sigma_\FD$.
\end{definition}

\begin{example}
\label{ex:dm_transl}
The functional dependencies in Example~\ref{ex:BCNF} are translated with the FD-direct mapping into the following tIdCs, \\ i.e.\ $\dm{course[lecture,type,room],\{\left(lecture,type\ra room\right), \left(room \ra type \right)\}}$ outputs:

 \begin{align*}
    \left(\mbox{id} \;\;course\_room\;\;course\# room^- \circ course? \circ \left( \right. \right. & course\# lecture \circ course\_lecture?,  \\
    &  course\# type \circ course\_type? \left.\left.\right)\right) \\
     \left(\mbox{id}\;\;course\_type\;\;course\# type^- \circ course? \circ \left( \right. \right. & course\# room \circ course\_room? \left.\left.\right)\right) \qedhere
\end{align*}
\end{example}

\noindent We now combine the FD-direct mapping with the schema direct mapping to define a direct mapping from a relational schema to a $\DLAtid$ TBox.

\begin{definition}{(Relational to Description Logic direct mapping (R2DM))}
Given a relational schema $R\left[A_1,\ldots,A_n\right]$ and a set of FDs over $R$, the function $\rdm{R[U],\FD}$ outputs on the schema $\left(R\left[U\right],\FD\right)$ a $\DLAtid$ T-Box $\TRU$ with tIdCs $\Sigma$ as follows:

\begin{itemize}
 \item[(1)] First, we call $\sm{R\left[U\right]}$, which outputs $\left< \TRU, \sigma_{R\left[U\right]} \right>$.
 \item[(2)] Then, we call $\dm{R\left[U\right],\FD}$, which outputs $\Sigma_\FD$.
\end{itemize}

\noindent The function $\rdm{R\left[U\right],FD}$ outputs $\left< \TRU, \{ \sigma_{R\left[U\right]} \} \cup \Sigma_\FD \right>$.
\end{definition}

\begin{example}
\label{ex:rdm_transl} $\ffo{rdm}\left(course[lecture,type,room],\left\{\left(lecture,type\ra room\right), \left(room \ra \right.\right.\right.$ \linebreak $\left.\left.\left. type \right)\right\}\right)$ outputs all assertions specified in Example~\ref{ex:sm_transl} and Example~\ref{ex:dm_transl}.
\end{example}

\noindent We have established a connection between instances of relational schemas and models of the TBox generated by the R2DM. Now, we turn our attention to the FDs. The R2DM already defines a translation of FDs to tIdCs. We want to show that our direct mapping is semantics preserving. For this, we will prove the following theorem.

\begin{theorem}
\label{thm:inst_fdmap}
Let $\ifo{I}$ be an instance of a relational schema $R\left[U\right]$, let $\left<\TRU,\sigma_{R\left[U\right]} \right>$ be the result of $\sm{R[U]}$, and let $\FD$ be a set of functional dependencies over $R[U]$. Then,

$$\ifo{I} \models \FD \mbox{ iff } \im{R[U]}{\ifo{I}} \models \dm{R[U],\FD}$$
\end{theorem}

\begin{proof} $\;$
\begin{itemize}
  \item[($\Ra$)] Suppose $\ifo{I} \models \FD$ and assume towards a contradiction that $\im{R[U]}{\ifo{I}} \nmodels  \dm{R[U],\FD}$. Then there exists some IdC $\varphi \in  \dm{R[U],\FD}$, for which it holds that $\im{R[U]}{\ifo{I}} \nmodels \varphi$. By the definition of $\dm{}$, $\varphi$ is of the form \[\id{R\_A_i}{R\# A_i^- \circ R? \circ \left(R \# A_{j_1} \circ A_{j_1}?, \ldots, R \# A_{j_k} \circ A_{j_k}?\right)},\] representing the functional dependency $A_{j_1}, \ldots, A_{j_k} \ra A_i$.  Let $\pi$ denote the tree in the IdC $\varphi$. Since $\im{R[U]}{\ifo{I}}  \nmodels \varphi$, the model $\mfo{M}$ outputted by $\im{R[U]}{\ifo{I}}$ has two distinct $R\_A_i$ objects $o$, $o^\prime$, with $\pi^\mfo{M}\left(o\right) \cap \pi^\mfo{M}\left(o^\prime\right) \neq \emptyset$. Let $\{ d_{j_1}, \ldots, d_{j_k} \} \in \pi^\mfo{M}\left(o\right) \cap \pi^\mfo{M}\left(o^\prime\right)$. Figure~\ref{fig:fd_lemma} illustrates the submodel of $\mfo{M}$, which leads to a violation of $\varphi$. 
  
  \begin{figure}[t]
    \centering
    \input{figures/dl/lem_fd.tikz}
    \caption{Submodel of $\mfo{M}$, which violates $\varphi$}
 	\label{fig:fd_lemma}
 \end{figure}
 
  We now apply $\mi{}{}$ to $\mfo{M}$ and by Lemma~\ref{lem:drm_instance} $\mi{\TRU}{\mfo{M}} = \ifo{I}$. This instance $I$ has two tuples $t$ and $t^\prime$, s.t.\ $t[A_i] = o$ and $t^\prime[A_i] = o^\prime$. Additionally $t[A_{j_i}] = t[A_{j_i}]$, for all $i \in [1\ldots k]$. Therefore, $A_{j_1}, \ldots, A_{j_k} \ra A_i$ is not valid in $\ifo{I}$, i.e.\ $\ifo{I} \nmodels FD$, a contradiction.
  
  
  \item[($\La$)] Suppose $\im{R[U]}{\ifo{I}}  \models \dm{R[U],\FD}$ and assume towards a contradiction that $\ifo{I} \nmodels \FD$. Then, there is an FD $\sigma \in \FD$, s.t.\ $\ifo{I} \nmodels \sigma$, where $\sigma = A_{j_1}, \ldots, A_{j_k} \ra A_i$. Therefore, $\ifo{I}$ has two tuples $t$, $t^\prime$ with different values in the $A_i$ columns, but the tuples agree on the values in the $A_{j_1}, \ldots, A_{j_k}$ columns, i.e.\ $t[A_i] \neq t^\prime[A_i]$ and $t[A_{j_i}] = t^\prime[A_{j_i}]$ for all $i\in \left[1\ldots k\right]$.  $\im{R[U]}{\ifo{I}}$ outputs a model $\mfo{M}$, with two tuple identifiers $t$ and $t^\prime$, s.t.\ $t$ and $t^\prime$ are connected to the same $R\_A_{j_1}, \ldots, R\_A_{j_k}$ objects, but to different $R\_A_i$ objects (compare to Figure~\ref{fig:fd_lemma}). The function $\dm{}$ also translates $\sigma$ into the IdC \[\varphi_\sigma := \id{R\_A_i}{R\# A_i^- \circ R? \circ \left(R \# A_{j_1} \circ A_{j_1}?, \ldots, R \# A_{j_k} \circ A_{j_k}?\right)}.\] Since the submodel of $\mcM$ depicted in Figure~\ref{fig:fd_lemma} violates $\varphi_\sigma$, also $\mfo{M} \nmodels \varphi_\sigma$. This contradicts the assumption that $\im{R[U]}{\ifo{I}}  \models \dm{R[U],\FD}$. Therefore, $I\models FD$ \qedhere
\end{itemize}
\end{proof}

\begin{corollary}
\label{cor:model_idcmap}
Let $\left(R\left[U\right],\FD\right)$ be a relational schema, let  $\left<\TRU,\Sigma \right>$ be the result of \linebreak $\drm{R[U],\FD}$ and let $\mfo{M}$ be a model of $\left<\TRU,\Sigma \right>$. Then,

$$\mfo{M} \models \Sigma \mbox{ iff } \mi{\TRU}{\mfo{M}}  \models FD$$
\end{corollary}

\begin{proof}
Corollary~\ref{cor:model_idcmap} follows from Theorem~\ref{thm:inst_fdmap} and Corollary~\ref{cor:mappingSemantics}
\end{proof}

\noindent From Theorem~\ref{thm:inst_fdmap} and Corollary~\ref{cor:model_idcmap} it follows that the R2DM is \textbf{semantics preserving}.
\end{subsubsection}
\end{subsection}
\end{section}

\begin{section}{Normal Forms}
\label{sec:dl_nf}

In the previous section we have established tree-based identification constraints for modeling functional dependencies in $\DLA$ knowledge bases. We will now look for a generalization of BCNF, similar to XNF, for $\DLAtid$ KBs. BCNF describes redundancy based on FDs, XNF uses XFDs and we will look for redundancies based on tIdCs. In this section we will first look at what a ``redundancy'' is in the context of $\DLAtid$ KBs. Based on those insights, we will define Description Logic Normal Form (DLNF). In Section~\ref{sec:dl_bcnf} we will prove that whenever a relational schema is in BCNF, then the $\DLA$ KB, translated from this schema, is in DLNF.

\begin{subsection}{Redundancy in $\DLAtid$ KBs}
 Let us first look at the redundancy in the relational instance depicted in Figure~\ref{fig:relCourse3NF}, which is not in BCNF, as it is illustrated in Example~\ref{ex:BCNF}. The FD $room \ra type$ violates BCNF, thus $room$ is not a superkey of the relation $course$. The translation of this instance via the R2DM is given in Figure~\ref{fig:im_transl}. The translated tIdC is 
 \begin{align}\sigma := \id{course\_{type}}{course\#type^- \circ course? \circ course\#room \circ course\_room? }.\label{eqn:tidc_course}\end{align}
 \noindent We can query the information expressed by this tIdC using a modified CQ, generated by the translation of tIdCs to CQ. Such a query asks for all course types and rooms in a model and looks as follows: 

 \begin{align}
  q_\sigma\left(t,x,r\right) \la & course\_{type}\left(t\right), course\#type\left(t,x\right), course\left(x\right), \\ & course\#room\left(x,r\right), course\_room\left(r\right)
 \end{align}
 \noindent The query $q_\sigma$ over the model given in Figure~\ref{fig:im_transl} returns the following tuples:
 
 \begin{center}
 \begin{tabular}{l|l|l}
  \multicolumn{1}{c|}{t} & \multicolumn{1}{c|}{x} & \multicolumn{1}{c}{r} \\ \hline
  $c_{\textit{type,VO}}$ & $t_{\left<\textit{Algebra I, VO, HS1}\right>}$ & $c_{\textit{room,HS1}}$ \\
  $c_{\textit{type,UE}}$ & $t_{\left<\textit{Algebra I, UE, SEM1}\right>}$ & $c_{\textit{room,SEM1}}$ \\
  $c_{\textit{type,UE}}$ & $t_{\left<\textit{Economics I, UE, SEM1}\right>}$ & $c_{\textit{room,SEM1}}$
 \end{tabular}
 \end{center}
 
 \noindent The information that each room can only host courses of a particular type, enforced by the tIdC $\sigma$, is stored redundantly. If we now want to specify that the only lecture type in room ``SEM1'' is ``VO'', we need to update the role membership assertions of $course\#type$ several times. Thus, updating just one role membership assertion leads to an update anomaly. \\
 
 \noindent How can we avoid such a redundancy? BCNF asks if the left-hand side of an FD is a superkey of the relation. XML Normal Form asks that if some attribute $a$ is uniquely determined by another set of attributes, then the parent element of $a$ should also be uniquely determined by the same set of attributes. In $\DLAtid$ KBs we neither have a flat structure as in the relational model nor a hierarchical structure as in XML documents. The graph-like structure of $\DLAtid$ allows us to talk about the neighbors of an object. If we view XML documents as graphs, the parent element of an attribute can also be considered as neighbor. Therefore, we want to define $\DLAtid$ normal form based on the neighbors of an object, i.e.\ for each object $a$ that is uniquely determined by a set of objects reachable via a tree its neighboring objects are also uniquely determined by the same set of objects. We will formalize this notion in the next section.
\end{subsection}

\begin{subsection}{$\DLAtid$ Normal Form}
 Before we define $\DLAtid$ Normal Form, we need some preliminary notions. In particular, we need to define the set $\ffo{neighbors}$ of a tree $\tau$ and the $\ffo{subtrees}$ of a tree $\tau$. 
 
 \begin{definition}{(subtrees of $\tau$)} Let $\tau$ be a tree. Then, we denote by $\ffo{subtrees}\left(\tau, i\right)$ the subtrees of $\tau$ starting at depth $i$, where $0 \leq i \leq \ffo{depth}\left(\tau\right)-1$.
 \end{definition}

 \begin{definition}{(neighbors of $\tau$)} Let $\tau$ be a tree. Then, we denote by $\ffo{neighbors}\left(\tau\right)$ the concepts appearing at $\ffo{depth}$ 1 in $\tau$. If this is a concept test $B?$, then $B$ is in the set $\ffo{neighbors}\left(\tau\right)$. If this is a role $R$ then $\exists R$ is in the set $\ffo{neighbors}\left(\tau\right)$.
 \end{definition}

 \noindent Let $\sigma$ be a tIdC. Then, we denote by $\Pi\left(\sigma\right)$ the components of $\sigma$. The neighbors of a tIdC $\sigma$, denoted by $\ffo{neighbors}\left(\sigma\right)$, is the set of neighbors of all trees in $\Pi\left(\sigma\right)$.
 
 \begin{example}
  Let $\tau$ be the first component of the tIdC $\sigma$ given in Equation~\ref{eqn:tidc_course}. Then, \linebreak $\ffo{subtrees}\left(\tau,1\right)$ is the tree $course? \circ course\#room \circ course\_room?$. Since $\sigma$ has only one component, the neighbors of $\sigma$ are the same as the neighbors of $\tau$, i.e.\ $\ffo{neighbors}\left(\tau\right) = \{ course \}$.
 \end{example}
 
 \noindent We are now ready to define Description Logic Normal Form for $\DLAtid$ KBs. 

\begin{definition}{(Description Logic Normal Form (k-DLNF))}
  \label{def:DLNF}
  Let $\mcT$ be a $\DLA$ TBox and let $\Phi$ be a set of tIdCs over $\mcT$. Then $\left<\mcT,\Phi\right>$ is in $k$-DLNF if and only if for every nontrivial tIdC $\varphi$, s.t. $\left<\mcT,\phi\right> \models \varphi$ and the depth of every component in $\varphi$ is at most $k$, it is the case that for each $C \in neighbors(\varphi)$  it holds that $\left<\mcT,\Phi\right> \models \id{C}{\Pi^\prime(C)}$, where
   \begin{align*}\Pi^\prime(C) = \left\{ \ffo{subtrees}\left(\tau,1\right) \mid \ffo{neighbors}\left(\tau\right) = C \wedge \ffo{depth}\left(\tau\right)>1 \;\; \forall \tau \in \Pi\left(\varphi\right) \right\}. & \qedhere\end{align*}
\end{definition}

\noindent If $k$ is arbitrarily large we simply say that a KB with tIdCs is in DLNF. Notice that, every TBox $\mcT$ with tIdCs $\Phi$ is in $1$-DLNF. $k$-DLNF captures the intuition of a normal form for DLs given in the previous section. We said that if a concept $C$ is uniquely determined by another set of concepts, the neighbors of $C$ must be uniquely determined by the same set of concepts. Since tIdCs translated by the FD-direct mapping are of depth 2, we consider 2-DLNF as an equivalent notion for BCNF in DLs. In Section~\ref{sec:dl_bcnf} we will show that this is indeed the case. \\

\noindent It is important to talk only about nontrivial tIdCs, since every functional dependency $\funct{R}$ implies the tIdC $\id{\top}{R^- \circ R}$. Then, it might not be the case that also $\id{\exists R}{R}$ is implied. If we would force that $\id{\exists R}{R}$ is implied, then it would not be possible for two different individuals to be connected with an $R$ role to the same individual. For example, let us assume that the role $\rfo{firstname}$ connects a concept $\cfo{person}$ with its first name, hence $\rfo{firstname}$ is functional. If we also include trivial tIdCs this would imply, that all people with the same first name have to be the same persons.  

  \noindent We will now look at several examples. The first example shows a KB translated by the R2DM from a relational schema that is not in BCNF. 
  
  \begin{example}
  \label{ex:DLNFcourse}
  
   Let us consider the relational schema $course\left(lecture,type,room\right)$ as introduced in Example~\ref{ex:BCNF}. This relational schema is not in BCNF. We will show that the translation of this schema is also not in 2-DLNF. The FD $room \ra type$ leads to a violation of BCNF. The translated tIdC is given in Equation~\ref{eqn:tidc_course}. We need to show that $$\sigma^\prime = \id{course}{course? \circ course\# room \circ course\_room?}$$ is also implied by the TBox $\mcT_{course}$ given in Example~\ref{ex:sm_transl} and the set of tIdCs $\Sigma_{course}$ given in Example~\ref{ex:dm_transl}. We have seen in Example~\ref{ex:im_transl} that the interpretation depicted in Figure~\ref{fig:im_transl} is a model of $\left<\mcT_{course},\Sigma_{course}\right>$. Hence, it should also be a model of $\sigma^\prime$. Unfortunately, this is not the case. The objects $t_{\left<\textit{Algebra I, UE, SEM1}\right>}$ and $t_{\left<\textit{Economics I, UE, SEM1}\right>}$ are both identified by the object $c_{\textit{room,SEM1}}$. Therefore, $course$ is not in 2-DLNF. \\
   
   \noindent In the relational model a repair of the relational schema that is dependency preserving is not possible. In Example~\ref{ex:XNFcourse} we have seen a XML document of the same information that is both information and dependency preserving. The same information on courses was already modeled with the TBox $\mcT_c$ given in Example~\ref{ex:dl_tbox}. The translation of the FDs $\rfo{room} \ra \rfo{type}$ and $\rfo{room} \ra \rfo{building}$ are already covered by the functionality assertion $\funct{\rfo{for}}$ and \linebreak $\funct{\rfo{has\_room}^-}$, respectively. Therefore, we only need to specify a tIdC that models the FD $lecture, type \ra room$, which is:
   \begin{gather}\id{room}{\rfo{located}^-,\rfo{for}}. \label{eqn:room_tidc}\end{gather}
   We will now check if $\mcT_c$ is in 2-DLNF. Additionally, to the tIdC in Equation~\ref{eqn:room_tidc} the functionality assertions in $\mcT_c$ imply the following tIdCs:
   \begin{gather}
     \id{\top}{\rfo{for^-}} \\
     \id{\top}{\rfo{has\_room}} \\
     \id{\top}{\rfo{located^-}} \\
     \id{\top}{\rfo{@name^-}}
   \end{gather}
  \noindent Furthermore, this set of tIdCs implies the following tIdCs of depth 2:
  \begin{gather}
     \id{\top}{\rfo{for^-} \circ \rfo{located}^-} \\
     \id{\top}{\rfo{has\_room} \circ \rfo{located}^-} \\
     \id{room}{\rfo{located}^-,\rfo{for} \circ \rfo{for^-}}
  \end{gather}
  It is easy to see that for this set of tIdCs the condition imposed by 2-DLNF holds, i.e.\ the tIdCs $\id{\exists \rfo{located}^-}{\rfo{located}^-}$ and $\id{\exists \rfo{for}^-}{\rfo{for}^-}$ are also implied by the above set of tIdCs. Notice that the ABox $\mcA_c$ given in Figure~\ref{fig:ABox_course} viewed as an interpretation is a model of $\mcT_c$ and does not contain any redundant information.
  \end{example}
  
  \noindent The second example shows how to check DLNF for an arbitrary $\DLAtid$ KB. Additionally, it recapitulates the intuition of DLNF.
 
 \begin{example}{(Football league \cite{2008calvanese})}

 \begin{figure}[t]
   \centering
   \includegraphics[width=0.7\textwidth]{figures/dl/football_ontology.png}
   \caption{Diagrammatic representation of the football leagues KB \cite{2008calvanese}.}
	\label{fig:ontFootball}
\end{figure}

\noindent Consider the football leagues KB from \cite{2008calvanese} depicted in Figure~\ref{fig:ontFootball}. Over this KB a possible tree-based identification assertion is
$$\id{league}{\textbf{year}, \rfo{BELONGS\mhyphen TO}^- \circ PLAYED\mhyphen IN^- \circ HOME},$$
\noindent which says that no home team plays in different leagues in the same year \cite{2008calvanese}. In order to test if the ontology in Figure~\ref{fig:ontFootball} is in DLNF, we have to prove that
$$\id{round}{PLAYED-IN^- \circ HOME}$$
\noindent is implied by the IdCs of the ontology. Such IdC states that no home team plays in different rounds, which is an implausible constraint. Therefore, the above ontology is not in DLNF. Now consider the BCNF intuition ``Do Not Represent the Same Fact Twice'' and the valid (up to the missing concepts) instance of the ontology depicted in Figure~\ref{fig:ontFootballInst}. Now consider again the tIdC $\id{league}{\textbf{year}, BELONGS\mhyphen TO^- \circ PLAYED\mhyphen IN^- \circ HOME}$. As we have seen, during the chase for implication of tIdCs, we can formulate a tIdC as a conjunctive query. Let us now consider the answer to the CQ~\ref{eqn:ontFootballQuery} over the ABox illustrated in Figure~\ref{fig:ontFootballInst} viewed as an interpretation. These answers are given in Table~\ref{tab:ontFootballAnswer}. We notice, that we have as answers two times the same information, which, having the BCNF intuition in mind, coincides to our intuition that the tIdC stated above leads to a violation of DLNF. \qedhere

\begin{align}
 league\_id(l,y,t) \la & league(l) \wedge year(l,y) \wedge BELONGS\mhyphen TO^-(l,x) \wedge \nonumber \\
                      & PLAYED\mhyphen IN^-(x,y) \wedge HOME(y,t) \label{eqn:ontFootballQuery}
\end{align}

\begin{table}[t]
 \centering
 \begin{tabular}{|l|l|l|}
  \hline \multicolumn{1}{|c|}{$l$} & \multicolumn{1}{c|}{$y$} & \multicolumn{1}{c|}{$t$} \\
  \hline \hline l1 & 2013 & t1  \\
  \hline l1 & 2013 & t1 \\ \hline
 \end{tabular}
 \caption{Answers to the CQ~\ref{eqn:ontFootballQuery} over the ontology instance in Figure~\ref{fig:ontFootballInst}.}
 \label{tab:ontFootballAnswer}
\end{table}

\begin{figure}[t]
   \centering
   \input{figures/dl/20130527-ontFootballInst.tikz}
   \caption{Diagrammatic representation of an ABox of the football leagues ontology.}
	\label{fig:ontFootballInst}
\end{figure}
\end{example}

\noindent These examples give us the following intuition for DLNF. Whenever a concept is uniquely determined by another set of concepts, then these concepts have to be reachable by a unique path or tree. With this observation one can conclude that for a $\DLAtid$ KB if all roles appearing in tIdCs are functional then this KB is in DLNF.

\end{subsection}

\end{section}

\begin{section}{BCNF - DLNF}
\label{sec:dl_bcnf}

Finally, we want to show that our definition of DLNF corresponds to BCNF in the relational model. This means that  if a relational schema is in BCNF then also the $\DLAtid$ KB generated by the R2DM is in 2-DLNF and vice versa. This is captured by the following theorem.

\begin{theorem}
\label{thm:BCNFDLNF} Let $R[U]$ be a relational schema and $\FD$ a set of functional dependencies over $R[U]$. Let $\left< \TRU,\Sigma \right>$ denote the output of the function $\drm{R[U],\FD}$. Then $(R[U],\FD)$ is in BCNF iff $\left< \TRU,\Sigma \right>$ is in $2$-DLNF.
\end{theorem}

\noindent Before we start with the proof for the theorem we observe the following. According to the relational-direct mapping we only have the two types of tIdCs in the set $\Sigma_\FD$: 

\begin{itemize}
 \item $\id{R\_A_i}{R\#A_i^- \circ \left( R\#A_{i_1}, \ldots, R\#A_{i_n}\right)}$,
 \item $\id{R}{R\#A_1, \ldots, R\#A_n}$.
\end{itemize}

\noindent Also notice that, because of $(\mbox{funct } R\#A_i)$ in the TBox of the R2DM the tIdCs \linebreak $$\id{\top}{R\#A_i^- \circ \left( R\#A_{i_1}, \ldots, R\#A_{i_n}\right)}$$ \noindent and $$\id{R\_A_i}{R\#A_i^- \circ R\#A_{i_1}, \ldots, R\#A_i^- \circ R\#A_{i_n}}$$ are equivalent. Additionally, because of concept disjointness, we never encounter in a tree an inverse role only after either the same forward role, or at the beginning of a path or tree. For example, $\id{R}{R\#A_1 \circ R\#A_2^-}$ is satisfied in all models of the created TBox, since the object after $R\#A_1$ would be inferred to be an instance of the concept $R\_A_1$ and $R\_A_2$, which contradicts the TBox assertion: $R\_A_1 \sqsubseteq \neg R\_A_2$. We also need the following lemma:

\begin{lemma}
\label{lem:IdCmapping}
$$A_1,\ldots, A_k \ra B \in (R[U],\FD)^+$$
\begin{center}if and only if\end{center}
$$\left<\TRU,\Sigma_{\FD}\right> \models \id{R\_B}{R\# B^- \circ R? \circ \left( R\# A_1, \ldots, R\# A_k \right)}.$$
\end{lemma}

\begin{proof}
Follows from Theorem~\ref{thm:inst_fdmap} and Corollary~\ref{cor:model_idcmap}.
\end{proof}

\noindent And finally, we can establish a proof for Theorem~\ref{thm:BCNFDLNF}:

\begin{proof}$\;$
\begin{itemize}  
  \item[($\La$)] Suppose $\left<\mcT_R,\Sigma_{\FD}\right>$ is in DLNF. We have to show that $\left(R[U],\FD\right)$ is in BCNF. Suppose that there are attributes $\{A_{i_1}, \ldots, A_{i_n}, A_i \} \subseteq U$, s.t. $A_{j_1}, \ldots, A_{j_k} \ra A_i$ is a nontrivial functional dependency in $(R[U],\FD)^+$. We have to prove that $A_{j_1}, \ldots, A_{j_k} \ra U \in (R[U],\FD)^+$. By Lemma~\ref{lem:IdCmapping} we know that \linebreak $\left<\mcT_R,\Sigma_{\FD}\right> \models \id{R\_ A_i}{R\# A_i^- \circ \left(R\# A_{j_1}, \ldots, R\# A_{j_k}\right)}$. Since, $\left<\mcT_R,\Sigma_{\FD}\right>$ is in 2-DLNF and $neighbors(R\_ A_i) = \{R\}$, also $\left<\mcT_R,\Sigma_{\FD}\right> \models \id{R}{R\# A_{j_1}, \ldots, R\# A_{j_k}}$. Since $(\mbox{funct } R\# A_i) \models \id{\top}{R\# A_i^-}$ also $\left<\mcT_R,\Sigma_{\FD}\right> \models \left(\mbox{id} \;\; A_i \;\; R\# A_i^- \circ \right.$ \linebreak $\left. \left(R\# A_{j_1}, \ldots, R\# A_{j_k}\right)\right)$ for all $A_i \in U$. By Lemma~\ref{lem:IdCmapping} also $A_{i_1}, \ldots, A_{i_k} \ra A_i$ for all $A_i \in U$, which proves that $\left(R[U],\FD\right)$ is in BCNF.
  
  \pagebreak
  
    \item[($\Ra$)] Suppose $\left(R[U],\FD\right)$ is in BCNF. We have to show that $\left<\mcT_R,\Sigma_\FD\right>$ is in $2$-DLNF. We distinguish two cases:
     \begin{itemize}
       \item Let $\varphi_1 = \id{R\_A_i}{R\# A_i^- \circ (R\#A_{i_1}, \ldots, R\#A_{i_k})}$, such that $\left<\mcT_R,\Sigma_\FD\right> \models \varphi_1$:\\
       
       \noindent We need to show that $\left<\mcT_R,\Sigma_\FD\right> \models \id{R}{R\#A_{i_1}, \ldots, R\#A_{i_k}}$. By Lemma~\ref{lem:IdCmapping} $A_{i_1}, \ldots, A_{i_k} \ra A_i \in (R[U],\FD)^+$. Since $\left(R[U],\FD\right)$ is in BCNF, also \linebreak $A_{i_1}, \ldots, A_{i_k} \ra U \in (R[U],\FD)^+$, i.e.\ for all $A_l \in U$ $A_{i_1}, \ldots, A_{i_k} \ra A_l \in (R[U],\FD)^+$. Therefore, by Lemma~\ref{lem:IdCmapping}, for all $R\_A_l$, $$\left<\mcT_R,\Sigma_\FD\right> \models \id{R\_A_l}{R\#A_l^- \circ (R\#A_{i_1}, \ldots, R\#A_{i_k})}.$$
       
       \noindent This IdC together with the IdC $\id{R}{R\#A_1, \ldots, R\#A_n}$ imply that $$\left<\mcT_R,\Sigma_\FD\right> \models \id{R}{R\#A_{i_1}, \ldots, R\#A_{i_k}},$$ which proves that $\left<\mcT_R,\Sigma_\FD\right>$ is in $2$-DLNF.
      
       
        \item Let $\left<\mcT_R,\Sigma_\FD\right> \models \id{R}{R\# A_{j_1} \circ R\# A_{j_1}^-, \ldots, R\# A_{j_k} \circ R\# A_{j_k}^-}$:
        
        \noindent We need to show for all $i \in [1\ldots k]$ that $\left<\mcT_R,\Sigma_\FD\right> \models \id{R\_A_{j_i}}{R\# A_{j_i}}$. Since $(\mbox{funct } R\#A_i)$ is in $\mcT_R$ and is equivalent to $\id{\top}{R\#A_i^-}$, the IdCs \linebreak $\id{R\_A_{j_i}}{R\# A_{j_i}}$ are trivially implied by $\mcT_R$. Therefore $\left<\mcT_R,\Sigma_\FD\right>$ is in $2$-DLNF. \qedhere
     \end{itemize}
\end{itemize}
\end{proof}

% \noindent It remains to ask whether a such a translated $\DLAtid$ KB is also in $k$-DLNF where $k > 2$. Unfortunately, the next example shows that this is not the case.
% 
% \begin{example}
% \label{ex:BCNFDLNF_problem}
% Consider the relational schema $R\left[ABCDE\right]$ with the functional dependencies (also converted to tIdCs)
% \begin{align*}
%  AB &\ra C & \id{R\_C}{R\#C^- \circ (R\#A, R\#B)} \\
%  DE &\ra A & \id{R\_A}{R\#A^- \circ (R\#D, R\#E)}
% \end{align*}
% \noindent Clearly, the following tIdC is implied by the above tIdCs:
% \begin{align}
%  BDE &\ra C & \id{R\_C}{R\#C^- \circ (R\#A \circ R\#A^- \circ (R\#D, R\#E) , R\#B)} \label{eqn:BDEAC}
% \end{align}
% \noindent If we now want to test DLNF with the implied tIdC given in Equation~\ref{eqn:BDEAC}, we need to check if
% \begin{align}
% \id{R}{R\#A \circ R\#A^- \circ (R\#D, R\#E) , R\#B)} \label{eqn:BDER} 
% \end{align}
% \noindent is implied by our set of tIdCs. We check for the implication using the method established in Section~\ref{sssec:tidcs_impl}. First, we build the counter-model ABox depicted in Figure~\ref{fig:BCNFDLNF_prob1}. Then, the tIdC $\id{R\_C}{R\#C^- \circ (R\#A, R\#B)}$ merges $a_1$ and $a_2$ to the model depicted in Figure~\ref{fig:BCNFDLNF_prob2}. Finally, the tIdC $\id{R\_A}{R\#A^- \circ (R\#D, R\#E)}$ merges $c_1$ and $c_2$ to the model depicted in Figure~\ref{fig:BCNFDLNF_prob2}. No more actions can be taken, therefore the tIdC in Equation~\ref{eqn:BDER} is not implied by this set of tIdCs.\end{example}
%   
% \begin{figure}[htbp]
% \begin{center}
% \input{figures/dl/20130725_problem.tikz} 
% \end{center}
% \caption{Counter-model ABox for the tIdC in Equation~\ref{eqn:BDER} - Step 1.} 
% \label{fig:BCNFDLNF_prob1}
% \end{figure}
%   
% \begin{figure}[htbp]
% \begin{center}
% \input{figures/dl/20130725_problem_2.tikz} 
% \end{center}
% \caption{Counter-model ABox for the IdC in Equation~\ref{eqn:BDER} - Step 2.} 
% \label{fig:BCNFDLNF_prob2}
% \end{figure}
% 
% \begin{figure}[htbp]
% \begin{center}
% \input{figures/dl/20130725_problem_3.tikz} 
% \end{center}
% \caption{Counter-model ABox for the IdC in Equation~\ref{eqn:BDER} - Step 3.} 
% \label{fig:BCNFDLNF_prob3}
% \end{figure}

\end{section}

\begin{section}{Summary}
  In this chapter we have recalled the Description Logic $\DLA$ as a formalism for graph databases. A $\DLA$ KB is constituted of a $\DLA$ TBox $\mcT$, which specifies general knowledge of a domain of interest, and a $\DLA$ ABox, which specifies knowledge of individuals in a domain. The models of a $\DLA$ KB are given in terms of interpretations. We have considered different reasoning services in $\DLA$, among them are KB satisfiability and query answering. For KB satisfiability we have introduced the notion of a $\DLA$ chase. We have seen that the chase terminates if the PI in the KB are weakly-acyclic. For query answering we have given two different methods. On the one hand, the chase can be used to materialize the canonical model, which then allows one to directly query this model. On the other hand, the perfect rewriting method allows one to include all assertions of a TBox into the query, which is then evaluated over the ABox. \\
  
  \noindent We have then introduced a direct-mapping from a relational schema to a $\DLA$ TBox. Additionally, we can also translate instances of a relational schema to models of such a $\DLA$ TBox. Since an equivalent to functional dependencies is missing in $\DLA$, we introduced path-based identification constraints. We have investigated KB satisfiability and implication of pIdCs in $\DLA$. Unfortunately, pIdCs are not the ideal candidate. It was shown that the direct-mapping extended with pIdCs is not semantics preserving. Therefore, we introduced tree-based identification constraints as an extension to pIdCs. KB satisfiability and implication of tIdCs can be solved similar as with pIdCs. We have then shown that the direct-mapping extended with tIdCs, called relational to Description Logic direct-mapping (R2DM) is semantics preserving. \\
  
  \noindent Finally, we investigated redundancies in $\DLA$ and established $k$-DLNF as an analogon to BCNF in $\DLA$ with tIdCs. We have shown that if a relational schema is in BCNF then the $\DLA$ KB, translated by the R2DM from the relational schema, is in 2-DLNF and vice versa.
\end{section}
